|
(scott_continuity
(lub_set_image 0
(lub_set_image-1 nil 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"
(inst - "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"
(skosimp*)
(("2"
(replace -1)
(("2"
(replace -2)
(("2"
(expand "directed?")
(("2"
(inst - "x!2" "x!3")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst + "g!1(z!1)")
(("1"
(expand "increasing?")
(("1"
(inst-cp
-
"x!2"
"z!1")
(("1"
(inst
-
"x!3"
"z!1")
(("1"
(assert)
(("1"
(assert)
nil
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))
nil))
nil))
nil))
nil))
nil))
nil)
((directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(le1 formal-const-decl "(directed_complete_partial_order?[T1])"
scott_continuity nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil scott_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(lub_set? const-decl "bool" bounded_order_props "orders/")
(directed_complete? const-decl "bool" directed_orders "orders/")
(z!1 skolem-const-decl "(D!1)" scott_continuity nil)
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "T1" scott_continuity nil)
(empty? const-decl "bool" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(g!1 skolem-const-decl "(increasing?)" scott_continuity nil)
(D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
(image const-decl "set[R]" function_image nil)
(directed? const-decl "bool" directed_orders "orders/")
(partial_order? const-decl "bool" orders nil)
(increasing? const-decl "bool" fun_preds_partial nil)
(le2 formal-const-decl "(directed_complete_partial_order?[T2])"
scott_continuity nil)
(T2 formal-type-decl nil scott_continuity nil))
shostak))
(directed_image_TCC1 0
(directed_image_TCC1-1 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)
((directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(le1 formal-const-decl "(directed_complete_partial_order?[T1])"
scott_continuity nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil scott_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(image const-decl "set[R]" function_image nil)
(x!1 skolem-const-decl "T1" scott_continuity nil)
(D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
(T2 formal-type-decl nil scott_continuity nil)
(le2 formal-const-decl "(directed_complete_partial_order?[T2])"
scott_continuity nil)
(increasing? const-decl "bool" fun_preds_partial nil))
nil))
(directed_image 0
(directed_image-1 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)
((""
(inst + "g!1(z!1)")
(("1"
(expand "increasing?")
(("1"
(inst-cp - "x!2" "z!1")
(("1"
(inst - "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)
((directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(le1 formal-const-decl "(directed_complete_partial_order?[T1])"
scott_continuity nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil scott_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(g!1 skolem-const-decl "(increasing?)" scott_continuity nil)
(D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
(z!1 skolem-const-decl "(D!1)" scott_continuity nil)
(image const-decl "set[R]" function_image nil)
(directed? const-decl "bool" directed_orders "orders/")
(increasing? const-decl "bool" fun_preds_partial nil)
(le2 formal-const-decl "(directed_complete_partial_order?[T2])"
scott_continuity nil)
(T2 formal-type-decl nil scott_continuity nil))
shostak))
(lub_image_TCC1 0
(lub_image_TCC1-1 nil 3352749145
("" (skosimp)
(("" (lemma "lub_set_image" ("g" "g!1" "D" "D!1"))
(("" (propax) nil nil)) nil))
nil)
((increasing? const-decl "bool" fun_preds_partial nil)
(le2 formal-const-decl "(directed_complete_partial_order?[T2])"
scott_continuity nil)
(T2 formal-type-decl nil scott_continuity nil)
(directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(le1 formal-const-decl "(directed_complete_partial_order?[T1])"
scott_continuity nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil scott_continuity nil)
(lub_set_image formula-decl nil scott_continuity nil))
nil))
(lub_image 0
(lub_image-1 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"
(hide -1 -2 -3)
(("2"
(typepred "g!1")
(("2"
(typepred "lub(D!1)")
(("1"
(expand "least_upper_bound?")
(("1"
(flatten)
(("1"
(hide -2)
(("1"
(expand "upper_bound?")
(("1"
(inst - "x!1")
(("1"
(expand
"increasing?")
(("1"
(inst
-
"x!1"
"lub(D!1)")
(("1"
(assert)
nil
nil)
("2"
(typepred "le1")
(("2"
(expand
"directed_complete_partial_order?")
(("2"
(flatten)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "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)
((directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(le1 formal-const-decl "(directed_complete_partial_order?[T1])"
scott_continuity nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil scott_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(image const-decl "set[R]" function_image nil)
(lub const-decl
"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
bounded_order_props "orders/")
(lub_set? const-decl "bool" bounded_order_props "orders/")
(least_upper_bound? const-decl "bool" bounded_orders "orders/")
(upper_bound? const-decl "bool" bounded_orders "orders/")
(directed_image formula-decl nil scott_continuity nil)
(T2 formal-type-decl nil scott_continuity nil)
(le2 formal-const-decl "(directed_complete_partial_order?[T2])"
scott_continuity nil)
(increasing? const-decl "bool" fun_preds_partial nil))
shostak))
(lub_image_increasing_TCC1 0
(lub_image_increasing_TCC1-1 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)
((directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(le1 formal-const-decl "(directed_complete_partial_order?[T1])"
scott_continuity nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil scott_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(empty? const-decl "bool" sets nil)
(T2 formal-type-decl nil scott_continuity nil)
(image const-decl "set[R]" function_image nil)
(x!1 skolem-const-decl "T1" scott_continuity nil)
(D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
(member const-decl "bool" sets nil))
nil))
(lub_image_increasing_TCC2 0
(lub_image_increasing_TCC2-1 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)
((directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(le1 formal-const-decl "(directed_complete_partial_order?[T1])"
scott_continuity nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil scott_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil scott_continuity nil)
(le2 formal-const-decl "(directed_complete_partial_order?[T2])"
scott_continuity nil)
(partial_order? const-decl "bool" orders nil)
(directed? const-decl "bool" directed_orders "orders/")
(image const-decl "set[R]" function_image nil)
(D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
(f!1 skolem-const-decl "[T1 -> T2]" scott_continuity nil)
(directed_complete? const-decl "bool" directed_orders "orders/")
(lub_set? const-decl "bool" bounded_order_props "orders/"))
nil))
(lub_image_increasing 0
(lub_image_increasing-1 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"
(flatten)
(("1"
(expand "reflexive?")
(("1" (inst - "f(y)") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace
"image(f,X) = LAMBDA (z:T2): z = f(x) OR z = f(y)")
(("1"
(name-replace "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"
(split -1)
(("1" (assert) nil nil)
("2"
(typepred "lub[T2, le2](Y)")
(("2"
(expand "least_upper_bound?")
(("2"
(flatten)
(("2"
(expand "upper_bound?")
(("2"
(inst - "f(x)")
(("1" (assert) nil nil)
("2"
(expand "Y")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(typepred "lub[T2, le2](Y)")
(("2"
(expand "least_upper_bound?")
(("2"
(flatten)
(("2"
(expand "upper_bound?")
(("2"
(inst - "f(y)")
(("1"
(typepred "le2")
(("1"
(expand
"directed_complete_partial_order?")
(("1"
(expand
"partial_order?")
(("1"
(expand
"antisymmetric?")
(("1"
(flatten)
(("1"
(inst
-
"lub[T2, le2](Y)"
"f(y)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "Y")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(assert)
(("3"
(typepred "le2")
(("3"
(expand
"directed_complete_partial_order?")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(expand "lub_set?")
(("2"
(typepred "le2")
(("2"
(expand
"directed_complete_partial_order?")
(("2"
(expand "directed_complete?")
(("2"
(flatten)
(("2"
(inst - "Y")
(("2"
(expand "directed?")
(("2"
(skosimp)
(("2"
(expand "directed?")
(("2"
(inst
-8
"x!1"
"y!1")
(("2"
(assert)
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))
nil))
nil))
nil)
("2" (apply-extensionality 1 :hide? t)
(("2" (expand "image")
(("2"
(hide-all-but 1)
(("2"
(case-replace
"EXISTS (x: (X)): x!1 = f(x)")
(("1"
(skosimp)
(("1"
(typepred "x!2")
(("1"
(expand "X")
(("1"
(split -1)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(replace 1 2)
(("2"
(assert)
(("2"
(split -1)
(("1"
(inst + "x")
(("1"
(expand "X")
(("1" (propax) nil nil))
nil))
nil)
("2"
(inst + "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"
(typepred "lub[T1, le1](X)")
(("2"
(replace -4)
(("2"
(expand "least_upper_bound?")
(("2"
(flatten)
(("2"
(expand "upper_bound?")
(("2"
(inst + "y")
(("1"
(inst-cp - "x!1")
(("1"
(inst - "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"
(inst -1 "y")
(("1"
(split -2)
(("1"
(typepred "le1")
(("1"
(expand
"directed_complete_partial_order?")
(("1"
(expand "partial_order?")
(("1"
(flatten)
(("1"
(expand "antisymmetric?")
(("1"
(inst
-
"lub[T1, le1](X)"
"y")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(typepred "r!1")
(("2"
(expand "X")
(("2"
(split -1)
(("1" (assert) nil nil)
("2"
(typepred "le1")
(("2"
(expand
"directed_complete_partial_order?")
(("2"
(expand
"partial_order?")
(("2"
(expand "preorder?")
(("2"
(flatten)
(("2"
(expand
"reflexive?")
(("2"
(inst - "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"
(skosimp)
(("1"
(typepred "r!1")
(("1"
(expand "X")
(("1"
(split -1)
(("1" (assert) nil nil)
("2"
(typepred "le1")
(("2"
(expand
"directed_complete_partial_order?")
(("2"
(expand "partial_order?")
(("2"
(expand "preorder?")
(("2"
(flatten)
(("2"
(expand "reflexive?")
(("2"
(inst - "y")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst - "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)
((increasing? const-decl "bool" fun_preds_partial nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil scott_continuity nil)
(least_bounded_above? const-decl "bool" bounded_orders "orders/")
(lub const-decl
"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
bounded_order_props "orders/")
(least_upper_bound? const-decl "bool" bounded_orders "orders/")
(y!1 skolem-const-decl "T1" scott_continuity nil)
(x!1 skolem-const-decl "T1" scott_continuity nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(image const-decl "set[R]" function_image nil)
(directed? const-decl "bool" directed_orders "orders/")
(directed_complete? const-decl "bool" directed_orders "orders/")
(Y skolem-const-decl "[T2 -> boolean]" scott_continuity nil)
(f skolem-const-decl "[T1 -> T2]" scott_continuity nil)
(x skolem-const-decl "T1" scott_continuity nil)
(upper_bound? const-decl "bool" bounded_orders "orders/")
(y skolem-const-decl "T1" scott_continuity nil)
(antisymmetric? const-decl "bool" relations nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(le2 formal-const-decl "(directed_complete_partial_order?[T2])"
scott_continuity nil)
(partial_order? const-decl "bool" orders nil)
(reflexive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(T2 formal-type-decl nil scott_continuity nil)
(directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(X skolem-const-decl "[T1 -> boolean]" scott_continuity nil)
(nonempty? const-decl "bool" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(partial_order_antisymmetric formula-decl nil partial_order_props
"orders/")
(partial_order_reflexive formula-decl nil partial_order_props
"orders/")
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(le1 formal-const-decl "(directed_complete_partial_order?[T1])"
scott_continuity nil)
(lub_set? const-decl "bool" bounded_order_props "orders/"))
shostak))
(scott_continuous_def 0
(scott_continuous_def-1 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"
(lemma "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"
(lemma
"down_is_closed[T2,le2]"
("x" "JFD"))
(("1"
(expand "member")
(("1"
(rewrite
"continuous_closed_sets")
(("1"
(inst - "down(JFD)")
(("1"
(expand "closed?")
(("1"
(expand "scott_open_sets")
(("1"
(expand "Complement")
(("1"
(expand "member")
(("1"
(split -10)
(("1"
(skosimp)
(("1"
(typepred "b!1")
(("1"
(rewrite
"complement_equal")
(("1"
(case
"subset?(D!1,b!1)")
(("1"
(expand
"scott_closed_sets")
(("1"
(expand
"extend")
(("1"
(prop)
(("1"
(inst
-
"D!1")
(("1"
(assert)
(("1"
(typepred
"lub[T2,le2](FD)")
(("1"
(replace
-7)
(("1"
(typepred
"lub(D!1)")
(("1"
(name
"JD"
"lub(D!1)")
(("1"
(replace
-1)
(("1"
(expand
"least_upper_bound?")
(("1"
(flatten)
(("1"
(expand
"increasing?")
(("1"
(inst
-5
"f!1(JD)")
(("1"
(split
-5)
(("1"
(expand
"inverse_image")
(("1"
(expand
"member")
(("1"
(replace
-9
-7
rl)
(("1"
(assert)
(("1"
(expand
"down")
(("1"
(lemma
"partial_order_antisymmetric"
("x"
"f!1(JD)"
"y"
"JFD"))
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"upper_bound?")
(("2"
(skosimp)
(("2"
(typepred
"r!1")
(("2"
(replace
-12
-1
rl)
(("2"
(expand
"image")
(("2"
(skosimp)
(("2"
(replace
-1)
(("2"
(inst
-18
"x!1"
"JD")
(("2"
(inst
-3
"x!1")
(("2"
(assert)
nil
nil))
nil))
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))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"subset?")
(("2"
(skosimp)
(("2"
(expand
"member")
(("2"
(replace
-3
1
rl)
(("2"
(expand
"inverse_image")
(("2"
(expand
"member")
(("2"
(expand
"down")
(("2"
(expand
"JFD")
(("2"
(typepred
"lub[T2, le2](FD)")
(("2"
(expand
"least_upper_bound?")
(("2"
(flatten)
(("2"
(expand
"upper_bound?")
(("2"
(inst
-
"f!1(x!1)")
(("2"
(expand
"FD")
(("2"
(expand
"image")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.82 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
