Impressum Cont.prf
Interaktion und
(Contnil 3353048819"" (skosimp)"" (expand "sq_le" )"" (expand "subset?" )"" (expand "member" )"" (split)"1" (skosimp*)"1" (expand "graph" )"1" (expand "extend" )"1" (expand "LPartFun_to_SPartFun" )"1" (expand "graph" )"1" (prop)"1" (inst - "x!1`1" "x!1`2" )"1" (lemma "up_down" ("y" "c1!1(x!1`1)" ))"1" (lemma "up_down" ("y" "c2!1(x!1`1)" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (inst - "x!1`1" "x!1`2" )"2" (lemma "up_down" ("y" "c1!1(x!1`1)" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "(s1!1,s2!1)" )"2" (expand "graph" )"2" (expand "extend" )"2" (expand "LPartFun_to_SPartFun" )"2" (assert )"2" (expand "graph" )"2" (replace -2)"2" (rewrite "down_up" )"2" "2" replace -2 1 rl)"2" "up_down" "y" "c2!1(s1!1)" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" Cont nil )"bool" sets nil )nil lift_props "orders/" )"R" extend nil )"bool" functions nil )nil Cont nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil State nil )nil Cont nil )nil lift_adt nil )nil lift_props "orders/" )"SubsetPartialFunction" nil )"set[[X, Y]]" partial_function_props "scott/" )"bool" sets nil ))nil 3353051459"" (expand "partial_order?" )"" (expand "preorder?" )"" (split)"1" (expand "reflexive?" )"1" (skosimp)"1" (rewrite "sq_le_def" )"1" (rewrite "subset_reflexive" ) nil nil )) nil ))nil ))nil )"2" (expand "transitive?" )"2" (skosimp)"2" (rewrite "sq_le_def" )"2" (rewrite "sq_le_def" )"2" (rewrite "sq_le_def" )"2" (expand "subset?" )"2" (expand "member" )"2" (skosimp)"2" (inst - "x!2" )"2" (inst - "x!2" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "antisymmetric?" )"3" (skosimp)"3" (rewrite "sq_le_def" )"3" (rewrite "sq_le_def" )"3" (lemma "subset_antisymmetric[[State,State]]" )"3" (inst - "graph(x!1)" "graph(y!1)" )"3" (assert )"3" (lemma "graph_eq" )"3" (inst - "x!1" "y!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" orders nil )"bool" relations nil )nil sets_lemmas nil )nil partial_function_props "scott/" )"bool" relations nil )"bool" sets nil )"bool" sets nil )"bool" relations nil )nil Cont nil )nil Cont nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil State nil )nil lift_adt nil )nil Cont nil )"(partial_order?[set[T]])" nil )"set[[X, Y]]" partial_function_props "scott/" )nil PartialFunctionDefinitionsnil )set type-eq-decl nil sets nil )nil booleans nil )nil sets_lemmas nil )"bool" orders nil ))nil 3353058858 ("" (subtype-tcc) nil nil )"bool" sets nil )"bool" sets nil )"bool" sets nil ))nil ))nil 3353058858"" (skosimp)"" (split -1)"1" (rewrite "emptyset_is_empty?" )"1" (replace -1)"1" (expand "image" )"1" (expand "graph?" )"1" (skosimp)"1" (expand "Union" )"1" (skosimp)"1" (skosimp)"1" (typepred "a!1" )"1" (typepred "a!2" )"1" (skosimp)"1" (typepred "x!2" )"1" expand "emptyset" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "graph?" )"2" (skosimp)"2" (expand "Union" )"2" (skosimp*)"2" (typepred "a!1" )"2" (typepred "a!2" )"2" (expand "image" )"2" (skosimp*)"2" (typepred "x!2" )"2" (typepred "x!3" )"2" (replace -3)"2" (replace -4)"2" "2" expand "graph" )"2" expand "extend" )"2" expand "LPartFun_to_SPartFun" )"2" expand "graph" )"2" "2" expand "directed?" )"2" "x!2" "x!3" )"2" assert )"2" "2" "z!1" )"2" expand "sq_le" )"2" "x!1" "y2!1" )"2" "x!1" "y1!1" )"2" "up_down" "y" "x!2(x!1)" ))"2" "up_down" "y" "x!3(x!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" partial_function_props "scott/" )"set" sets nil )"set[[X, Y]]" partial_function_props "scott/" )nil PartialFunctionDefinitionsnil )"[T, T -> boolean]" equalities nil )"set" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"set[R]" function_image nil )"finite_set" finite_sets nil )"finite_set[Cont]" Cont nil )nil Cont nil )nil lift_adt nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil Cont nil )set type-eq-decl nil sets nil )nil booleans nil )nil sets_lemmas nil )"SubsetPartialFunction" nil )"bool" Cont nil )nil lift_props "orders/" )"bool" directed_orders "orders/" )"bool" functions nil )"R" extend nil ))nil ))nil 3353730711"" (skosimp)"" (case-replace "nonempty?(D!1)" )"1" (split -2)"1" (expand "nonempty?" ) (("1" (propax) nil nil )) nil )"2" (expand "least_upper_bound?" )"2" (split)"1" (expand "upper_bound?" )"1" (skosimp)"1" (expand "sq_le" )"1" (skosimp)"1" (expand "from_graph" )"1" (lift-if)"1" (assert )"1" (prop)"1" "{y: State | Union(image(graph, D!1))(s1!1, y)} = singleton(s2!1)" )"1" rewrite "choose_singleton" )nil nil )"2" "2" "2" expand "singleton" )"2" "x!1=s2!1" )"1" "r!1" )"1" expand "Union" )"1" "graph(r!1)" )"1" expand "graph" )"1" expand "extend" )"1" expand "LPartFun_to_SPartFun" )"1" expand "graph" )"1" replace -4)"1" rewrite "down_up" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" "r!1" )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "Union" )"2" "2" "a!1" )"2" expand "image" )"2" "2" "x!2" )"2" replace -2)"2" "2" "r!1" )"2" expand "directed?" )"2" "x!2" "r!1" )"2" assert )"2" "2" expand "graph" )"2" expand "extend" )"2" "2" expand "graph" )"2" expand "LPartFun_to_SPartFun" )"2" replace "2" "s1!1" "x!1" )"2" "s1!1" "s2!1" )"2" assert )"2" "1" "down_equal" "y1" "up(x!1)" "y2" "up(s2!1)" ))"1" assert )nil nil ))nil )"2" replace "2" "up_down" "y" "x!2(s1!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" expand "empty?" )"2" "2" expand "member" )"2" "s2!1" )"2" expand "Union" )"2" "graph(r!1)" )"1" expand "graph" )"1" expand "extend" )"1" expand "LPartFun_to_SPartFun" )"1" expand "graph" )"1" replace -1)"1" rewrite "down_up" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" "r!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "sq_le" )"2" (expand "upper_bound?" )"2" (skosimp*)"2" (expand "from_graph" )"2" (lift-if -2)"2" (assert )"2" (prop)"2" (copy -1)"2" (expand "nonempty?" -1)"2" expand "empty?" )"2" expand "member" )"2" "2" expand "Union" -1)"2" "2" "a!1" )"2" expand "image" -1)"2" "2" replace -1)"2" "x!2" )"2" "2" "x!2" )"2" "s1!1" "x!1" )"2" expand "graph" "2" expand "extend" )"2" expand "LPartFun_to_SPartFun" )"2" "1" expand "graph" "1" "{y:State|Union(image(graph,D!1))(s1!1,y)} =singleton(x!1)" )"1" rewrite "choose_singleton" )"1" assert )nil nil ))nil )"2" "2" "2" expand "singleton" )"2" "x!3 = x!1" )"1" expand "Union" )"1" "graph(x!2)" )"1" expand "graph" )"1" expand "extend" )"1" expand "LPartFun_to_SPartFun" )"1" expand "graph" )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" "x!2" )nil nil ))nil ))nil ))nil )"2" assert )"2" expand "Union" )"2" "2" "a!2" )"2" expand "image" )"2" "2" "x!4" )"2" replace "2" "2" expand "graph" )"2" expand "extend" )"2" expand "LPartFun_to_SPartFun" )"2" expand "graph" )"2" "2" "2" expand "directed?" )"2" "x!2" "x!4" )"2" assert )"2" "2" "s1!1" "x!1" )"2" "s1!1" "x!3" )"2" "up_down" "y" "x!4(s1!1)" ))"2" "up_down" "y" "x!2(s1!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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "graph" )"2" "up_down" "y" "x!2(s1!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (hide -2)"2" "from_graph(Union(image(graph, D!1))) = lambda (s:State): bottom" )"1" (rewrite "emptyset_is_empty?" )"1" (replace -2)"1" (hide -1 -2)"1" (expand "least_upper_bound?" )"1" (expand "upper_bound?" )"1" (expand "sq_le" )"1" (skosimp)"1" (typepred "r!1" )"1" (expand "emptyset" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (expand "image" )"2" (expand "Union" )"2" (expand "from_graph" )"2" (lift-if)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (prop)"2" "2" expand "member" )"2" "2" "a!1" )"2" "2" "x!3" )"2" "x!3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil Cont nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil State nil )nil lift_adt nil )nil Cont nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" bounded_orders "orders/" )"(D!1)" Cont nil )"bool" bounded_orders "orders/" )"bool" Cont nil )"LiftPartialFunction" partial_function_props"scott/" )"bool" sets nil )"bool" sets nil )"non_empty_finite_set" finite_sets nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )nil sets nil )"set" sets nil )nil PartialFunctionDefinitionsnil )"set[R]" function_image nil )"set[[X, Y]]" partial_function_props "scott/" )"bool" sets nil )"(singleton?)" sets nil )nil sets_lemmas nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"SubsetPartialFunction" nil )nil lift_props "orders/" )"bool" functions nil )"R" extend nil )"(D!1)" Cont nil )"set[Cont]" Cont nil )NOT const-decl "[bool -> bool]" booleans nil )"[T -> (up?)]" lift_adt nil )"[lift -> boolean]" lift_adt nil )nil lift_props "orders/" )nil lift_props "orders/" )"bool" directed_orders "orders/" )nil sets_lemmas nil )"finite_set[Cont]" Cont nil )"finite_set" finite_sets nil )"set" sets nil )"(bottom?)" lift_adt nil )"[lift -> boolean]" lift_adt nil )"bool" partial_function_props "scott/" ))nil 3353053412"" (expand "directed_complete_partial_order?" )"" (lemma "partial_order_sq_le" )"" (assert )"" (expand "directed_complete?" )"" (skosimp)"" (expand "least_bounded_above?" )"" (name "G" "Union(image(graph,D!1))" )"" (case "graph?(G)" )"1" (inst + "from_graph(G)" )"1" (expand "least_upper_bound?" )"1" (expand "upper_bound?" )"1" (expand "sq_le" )"1" (expand "G" )"1" (expand "from_graph" )"1" "1" "1" "1" "1" assert )"1" "1" "r!1" )"1" "down_equal" "y1" "up(choose({y: State | Union(image(graph, D!1))(s1!1, y)}))" "y2" "up(s2!1)" ))"1" "1" "1" "1" rewrite "down_up" "1" rewrite "down_up" "1" "1" nil nil )"2" "2" "choose_singleton" "x" "s2!1" ))"2" expand "singleton" )"2" "{y: State | Union(image(graph, D!1))(s1!1, y)} = {y: State | y = s2!1}" )"2" "2" "2" "x!1=s2!1" )"1" expand "Union" )"1" "graph(r!1)" )"1" expand "graph" )"1" expand "extend" )"1" expand "LPartFun_to_SPartFun" )"1" expand "graph" )"1" replace "1" rewrite "down_up" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" "r!1" )nil nil ))nil ))nil ))nil )"2" assert )"2" expand "Union" )"2" "2" "a!1" )"2" expand "image" )"2" "2" "x!2" )"2" replace "2" expand "graph" )"2" expand "extend" )"2" expand "LPartFun_to_SPartFun" )"2" "2" expand "graph" )"2" "2" "D!1" )"2" expand "directed?" )"2" expand "sq_le" )"2" "x!2" "r!1" )"2" assert )"2" "2" "z!1" )"2" "s1!1" "x!1" )"2" "up_down" "y" "x!2(s1!1)" ))"2" assert )"2" "s1!1" "s2!1" )"2" assert )"2" "down_equal" "y1" "up(x!1)" "y2" "up(s2!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" assert )nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" "r!1" )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "s2!1" )"2" expand "Union" )"2" "graph(r!1)" )"1" expand "graph" )"1" expand "extend" )"1" expand "LPartFun_to_SPartFun" )"1" expand "graph" )"1" replace "1" rewrite "down_up" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" "r!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "2" "2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "2" expand "member" )"2" expand "Union" )"2" "2" "a!1" )"2" expand "image" )"2" "2" "x!2" )"2" "x!2" )"2" replace "2" "2" "{y: State | EXISTS (a: (image(graph, D!1))): a(s1!1, y)} = singleton(x!1)" )"1" "1" rewrite "choose_singleton" )"1" "down_equal" "y1" "up(x!1)" "y2" "up(s2!1)" ))"1" assert )"1" replace "1" "s1!1" "s2!1" )"1" expand "graph" )"1" expand "extend" )"1" expand "LPartFun_to_SPartFun" )"1" expand "graph" )"1" "1" replace "1" "up_down" "y" "x!2(s1!1)" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "graph?" )"2" "2" expand "singleton" )"2" "x!3=x!1" )"1" "graph(x!2)" )"1" expand "image" )"1" "x!2" )nil nil ))nil ))nil )"2" assert )"2" "2" "a!2" )"2" expand "image" )"2" "2" replace "2" "2" "x!4" )"2" "2" "s1!1" "x!3" "x!1" )"2" "1" nil nil )"2" "graph(x!4)" )"2" expand "image" )"2" "x!4" )nil nil ))nil ))nil )"3" "graph(x!2)" )"3" expand "image" )"3" "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "D!1" )"2" (expand "directed?" )"2" (hide -3)"2" (expand "G" )"2" (expand "graph?" )"2" "2" expand "image" )"2" expand "Union" )"2" "2" "a!1" )"2" "a!2" )"2" "2" replace -1)"2" replace -2)"2" "2" expand "graph" )"2" expand "extend" )"2" expand "LPartFun_to_SPartFun" )"2" expand "graph" )"2" "2" "x!2" )"2" "x!3" )"2" "x!2" "x!3" )"2" assert )"2" "2" expand "sq_le" )"2" "x!1" "y2!1" )"2" "x!1" "y1!1" )"2" assert )"2" "up_down" "y" "x!3(x!1)" ))"2" "up_down" "y" "x!2(x!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil Cont nil )"bool" directed_orders "orders/" )"bool" bounded_orders "orders/" )"bool" partial_function_props "scott/" )"bool" bounded_orders "orders/" )"(D!1)" Cont nil )"(D!1)" Cont nil )"non_empty_finite_set" finite_sets nil )"bool" sets nil )nil lift_props "orders/" )nil defined_types nil )"boolean" lift_adt nil )"[lift -> boolean]" lift_adt nil )"[T -> (up?)]" lift_adt nil )"(p)" sets nil )nil lift_props "orders/" )nil sets_lemmas nil )nil lift_props "orders/" )"SubsetPartialFunction" nil )"bool" functions nil )"R" extend nil )"(D!1)" Cont nil )"(directed?(sq_le))" Cont nil )"(singleton?)" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"bool" sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" bounded_orders "orders/" )"LiftPartialFunction" partial_function_props"scott/" )"set[[State[V], State[V]]]" Cont nil )nil Cont nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil State nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )nil sets nil )"set" sets nil ) (lift type-decl nil lift_adt nil )nil PartialFunctionDefinitionsnil )"set[R]" function_image nil )"set[[X, Y]]" partial_function_props "scott/" )nil Cont nil )"bool" sets nil )nil defined_types nil )"bool" orders nil )"bool" directed_orders "orders/" )"bool" Cont nil )"bool" directed_orders"orders/" )"(partial_order?[Cont])" Contnil ))nil 3353060450"" (expand "pointed_directed_complete_partial_order?" )"" (lemma "sq_le_dcpo" )"" (assert )"" (expand "fullset" )"" (hide -1)"" (expand "sq_le" )"" (expand "has_least?" )"" (inst + "lambda s: bottom" )"" (expand "least?" )"" (expand "lower_bound?" )"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil Cont nil )"set" sets nil )"bool" Cont nil )nil Cont nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil State nil )nil lift_adt nil )nil Cont nil )"[lift -> boolean]" lift_adt nil )"(bottom?)" lift_adt nil )"bool" bounded_orders "orders/" )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"bool" "orders/" )"(partial_order?[Cont])" Contnil )"(directed_complete_partial_order?[Cont])" Cont nil ))nil 3353817335"" (expand "sq_le" ) (("" (propax) nil nil )) nil )"bool" Cont nil )) shostak))nil 3353878044"" (expand "least?" )"" (expand "fullset" )"" (expand "lower_bound?" )"" (skosimp)"" (lemma "sq_le_bottom" ("c" "r!1" ))"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"set" sets nil )nil Cont nil )nil Cont nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil State nil )nil lift_adt nil )nil Cont nil )nil booleans nil )"bool" booleans nil )"bool" bounded_orders "orders/" )"bool" minmax_orders "orders/" ))nil 3354084506"" (skosimp)"" (expand "sq_le" )"" (expand "conditional" )"" (split)"1" (skosimp*)"1" (inst - "s1!1" "s2!1" )"1" (case-replace "p!1(s1!1)" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "s1!1" "s2!1" )"2" (assert )"2" (flatten)"2" (case-replace "p!1(s1!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" Cont nil )nil Cont nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil State nil )nil defined_types nil )nil booleans nil )"Cont" Cont nil ))nil 3355455917"" (skosimp)"" (expand "scott_continuous?" )"" (name-replace "G" "c1!1" )"" (name "F" "LAMBDA c: c o G" )"" (replace -1)"" (case-replace "increasing?(F)" )"1" (expand "lub_preserving?" )"1" (skosimp)"1" (lemma "lub_image" ("g" "F" "D" "D!1" ))"1" (typepred "sq_le" )"1" expand "pointed_directed_complete_partial_order?" )"1" expand "directed_complete_partial_order?" )"1" (expand "partial_order?" )"1" (flatten)"1" expand "antisymmetric?" )"1" "F(lub(D!1))" "lub(image(F, D!1))" )"1" assert )"1" "1" expand "F" 1)"1" "lub(D!1)" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" case "FORALL (r: Cont): ") "1" "lub(image(LAMBDA c: c o G, D!1))" )"1" "1" nil nil )"2" "2" "2" "r!1" )"2" replace "2" "lub(image(F, D!1))" )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" )"2" "r!1 o G" )"2" expand "image" )"2" "r!1" )"2" expand "F" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "DRL1" "lub(D!1)" )"2" expand "sq_le" )"2" "2" expand "o" "2" case "EXISTS (c:(D!1)): (c o G)(s1!1) = up(s2!1)" )"1" "1" "c!1" )"1" "s1!1" "s2!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "o " )"2" case "bottom?(G(s1!1))" )"1" assert )nil nil )"2" "X" "{c:(D!1)| c(down(G(s1!1))) = up(s2!1)}" )"1" case "nonempty?(X)" )"1" expand "nonempty?" )"1" expand "empty?" )"1" "1" expand "member" )"1" expand "X" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" expand "DRL1" )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "lub(D!1)" )"2" expand "least_upper_bound?" )"2" "2" case "FORALL (s: State, r1, r2: (D!1)): NOT bottom?(r1(s)) & NOT bottom?(r2(s))) => r1(s) = r2(s)") "1" "S" "down(G(s1!1))" )"1" case "forall (r:(D!1)): r(S) = bottom[State]" )"1" "lambda s: if s = S then bottom[State] else lub(D!1)(s) endif" )"1" "1" expand "sq_le" )"1" "S" "s2!1" )"1" assert )nil nil ))nil ))nil )"2" expand "upper_bound?" )"2" "2" expand "sq_le" )"2" "2" "r!2" )"2" "r!2" )"2" assert )"2" "s1!2=S" )"1" assert )nil nil )"2" assert )"2" "r!2" )"2" "s1!2" "s2!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "r!2" )"2" "lambda s: if s = S then r!2(s) else lub(D!1)(s) endif" )"2" "1" expand "sq_le" "1" "S" "s2!1" )"1" assert )"1" "r!2" )"1" expand "X" )"1" expand "S" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "upper_bound?" )"2" "2" "r!3" )"2" expand "sq_le" "2" "2" "s1!2 = S" )"1" "S" "r!2" "r!3" )"1" assert )nil nil ))nil )"2" assert )"2" expand "sq_le" "2" "r!3" )"2" "s1!2" "s2!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "r1!1" )"2" "r2!1" )"2" "D!1" )"2" expand "directed?" )"2" expand "directed?" )"2" "r1!1" "r2!1" )"2" assert )"2" "2" expand "sq_le" )"2" "s!1" "down(r1!1(s!1))" )"2" "s!1" "down(r2!1(s!1))" )"2" rewrite "up_down" )"2" rewrite "up_down" )"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 ))nil ))nil ))nil ))nil ))nil )"2" "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 ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "increasing?" )"2" (skosimp*)"2" (expand "sq_le" )"2" (skosimp)"2" (expand "F" )"2" (expand "o" )"2" (lift-if)"2" "bottom?(G(s1!1))" )"2" assert )"2" "down(G(s1!1))" "s2!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" scott_continuity "scott/" )"LiftPartialFunction[X, Z]" nil )nil PartialFunctionDefinitionsnil )"bool" fun_preds_partial "scott/" )"bool" Cont nil )nil booleans nil )"(partial_order?[Cont])" Contnil )"(directed_complete_partial_order?[Cont])" Cont nil )"(pointed_directed_complete_partial_order?[Cont])" Cont nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )"bool" "orders/" )"bool" directed_orders"orders/" )"bool" orders nil )"set[R]" function_image nil )"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" "orders/" )"bool" bounded_orders "orders/" )"bool" bounded_order_props "orders/" )"[bool, bool -> bool]" booleans nil )"Cont" Cont nil )"(D!1)" Cont nil )"directed[Cont, (sq_le)]" Cont nil )"[lift -> boolean]" lift_adt nil )"bool" sets nil )"bool" sets nil )"[(D!1) -> boolean]" Cont nil )"{x | bounded_orders[Cont].least_upper_bound?(x, D!1, (sq_le))}" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(bottom?)" lift_adt nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"State[V]" Cont nil )nil lift_props "orders/" )"bool" directed_orders "orders/" )"[(up?) -> T]" lift_adt nil )"[T -> (up?)]" lift_adt nil )"[lift -> boolean]" lift_adt nil )"bool" bounded_orders "orders/" )"[Cont -> LiftPartialFunction[State[V], State[V]]]" Cont nil )"clopen[Cont, scott_open_sets]" nil )"(partial_order?[[Cont -> Cont]])" Cont nil )"bool" relations nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"bool" sets nil )set type-eq-decl nil sets nil )nil scott_continuity "scott/" )"bool" scott_continuity "scott/" )"[T, T -> boolean]" equalities nil )nil Cont nil )nil lift_adt nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil Cont 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.143Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-28)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
