| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/scott/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 218 kB |
|
Quellcode-Bibliothek scott_continuity.prfSprache: Lisp |
|||||||||||||||
|
(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") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "down(JFD)") (("2" (typepred "le2") (("2" (expand "directed_complete_partial_order?") (("2" (flatten) 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)) 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" (inst - "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" (lemma "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" (skosimp) (("1" (typepred "b!1") (("1" (rewrite "complement_equal") (("1" (assert) (("1" (expand "inverse_image") (("1" (expand "member") (("1" (expand "lower_set?") (("1" (expand "member") (("1" (inst -2 "y!1" "x!1") (("1" (replace -6 -2 rl) (("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" (lemma "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" (prop) (("1" (name "X" "inverse_image(f!1, Y!1)") (("1" (replace -1) (("1" (inst + "complement(X)") (("1" (rewrite "complement_complement") nil nil) ("2" (expand "scott_closed_sets") (("2" (expand "extend") (("2" (lemma "complement_upper_set" ("U" "X")) (("1" (assert) (("1" (skosimp) (("1" (typepred "D!1") (("1" (replace -5 * rl) (("1" (expand "complement") (("1" (expand "member") (("1" (replace -12) (("1" (typepred "lub(D!1)") (("1" (inst -9 "image(f!1,D!1)") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (expand "lub_preserving?") (("1" (inst -11 "D!1") (("1" (split -11) (("1" (split -9) (("1" (assert) nil nil) ("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (expand "image") (("2" (skosimp) (("2" (typepred "x!2") (("2" (expand "lower_set?") (("2" (inst -8 "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "lub_set?") (("2" (lemma "directed_image" ("g" "f!1" "D" "D!1")) (("2" (typepred "le2") (("2" (expand "directed_complete_partial_order?") (("2" (flatten) (("2" (expand "directed_complete?") (("2" (inst - "image(f!1, D!1)") (("2" (expand "directed?" -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "directed_image" ("g" "f!1" "D" "D!1")) (("2" (assert) (("2" (hide-all-but (-3 1)) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (inst - "f!1(x!1)") (("2" (expand "member") (("2" (expand "image") (("2" (inst + "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" (prop) (("2" (expand "upper_set?") (("2" (expand "member") (("2" (expand "inverse_image") (("2" (skosimp) (("2" (expand "member") (("2" (replace -7) (("2" (expand "complement") (("2" (expand "member") (("2" (expand "lower_set?") (("2" (expand "member") (("2" (inst - "f!1(y!1)" "f!1(x!1)") (("2" (expand "increasing?") (("2" (inst - "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) ((scott_continuous? const-decl "bool" scott_continuity nil) (open? const-decl "bool" topology "topology/") (complement_upper_set judgement-tcc nil partial_order_props "orders/") (upper_set nonempty-type-eq-decl nil partial_order_props "orders/") (x!1 skolem-const-decl "T1" scott_continuity nil) (directed_complete? const-decl "bool" directed_orders "orders/") (partial_order? const-decl "bool" orders nil) (directed? const-decl "bool" directed_orders "orders/") (D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (complement_complement formula-decl nil sets_lemmas nil) (X skolem-const-decl "set[T1]" scott_continuity nil) (complement const-decl "set" sets nil) (upper_set? const-decl "bool" partial_order_props "orders/") (continuous_open_sets formula-decl nil continuity "topology/") (subset_of_Cl formula-decl nil topology "topology/") (Cl_closed formula-decl nil topology "topology/") (order_iff_closure formula-decl nil scott nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (FALSE const-decl "bool" booleans nil) (directed_singleton application-judgement "directed[T, <=]" scott_continuity nil) (scott_open_sets_is_topology name-judgement "topology" scott_continuity nil) (Cl const-decl "set[T]" topology "topology/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (lub_preserving? const-decl "bool" scott_continuity nil) (directed type-eq-decl nil directed_order_props "orders/") (directed? const-decl "bool" directed_order_props "orders/") (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (image const-decl "set[R]" function_image nil) (= const-decl "[T, T -> boolean]" equalities nil) (down_is_closed formula-decl nil scott nil) (scott_open_sets const-decl "setofsets[T]" scott nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (continuous_closed_sets formula-decl nil continuity "topology/") (closed? const-decl "bool" topology "topology/") (Complement const-decl "setofsets[T]" sets_lemmas nil) (scott_closed_sets const-decl "setofsets[T]" scott nil) (subset? const-decl "bool" sets nil) (extend const-decl "R" extend nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (partial_order_antisymmetric formula-decl nil partial_order_props "orders/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (Cl_is_closed application-judgement "closed[T, scott_open_sets]" scott_continuity nil) (singleton_is_compact application-judgement "compact[T, scott_open_sets]" scott_continuity nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" scott_continuity nil) (JFD skolem-const-decl "{x | bounded_orders[T2].least_upper_bound?(x, FD, le2)}" scott_continuity nil) (D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil) (x!1 skolem-const-decl "T1" scott_continuity nil) (f!1 skolem-const-decl "[T1 -> T2]" scott_continuity nil) (FD skolem-const-decl "set[T2]" scott_continuity nil) (complement_equal formula-decl nil sets_lemmas nil) (inverse_image const-decl "set[D]" function_image nil) (lower_set? const-decl "bool" partial_order_props "orders/") (lower_set nonempty-type-eq-decl nil partial_order_props "orders/") (down const-decl "lower_set" partial_order_props "orders/") (member const-decl "bool" sets nil) (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/") (lub_set? const-decl "bool" bounded_order_props "orders/") (closure_is_down formula-decl nil scott nil) (empty? const-decl "bool" sets nil) (x!1 skolem-const-decl "T1" scott_continuity nil) (directed_image formula-decl nil scott_continuity nil) (increasing? const-decl "bool" fun_preds_partial nil) (le2 formal-const-decl "(directed_complete_partial_order?[T2])" scott_continuity nil) (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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T2 formal-type-decl nil scott_continuity nil) (T1 formal-type-decl nil scott_continuity nil)) shostak)) (scott_continuous_is_continuous 0 (scott_continuous_is_continuous-1 nil 3330316834 ("" (skosimp) (("" (typepred "x!1") (("" (rewrite "scott_continuous_def") nil nil)) nil)) nil) ((scott_continuous? const-decl "bool" scott_continuity nil) (T2 formal-type-decl nil scott_continuity 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) (scott_continuous_def formula-decl nil scott_continuity nil)) shostak)) (continuous_is_scott_continuous 0 (continuous_is_scott_continuous-1 nil 3330316859 ("" (skosimp) (("" (typepred "x!1") (("" (rewrite "scott_continuous_def") nil nil)) nil)) nil) ((continuous? const-decl "bool" continuity_def "topology/") (le2 formal-const-decl "(directed_complete_partial_order?[T2])" scott_continuity nil) (scott_open_sets const-decl "setofsets[T]" scott nil) (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) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T2 formal-type-decl nil scott_continuity 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) (scott_continuous_def formula-decl nil scott_continuity nil)) shostak)) (continuous_is_increasing 0 (continuous_is_increasing-1 nil 3330547445 ("" (skosimp) (("" (typepred "x!1") (("" (rewrite "scott_continuous_def") (("" (expand "scott_continuous?") (("" (flatten) nil nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuity_def "topology/") (le2 formal-const-decl "(directed_complete_partial_order?[T2])" scott_continuity nil) (scott_open_sets const-decl "setofsets[T]" scott nil) (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) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T2 formal-type-decl nil scott_continuity 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) (scott_continuous? const-decl "bool" scott_continuity nil) (scott_continuous_def formula-decl nil scott_continuity nil)) shostak)) (continuous_is_lub_preserving 0 (continuous_is_lub_preserving-1 nil 3330934809 ("" (skosimp) (("" (typepred "x!1") (("" (rewrite "scott_continuous_def") (("" (expand "scott_continuous?") (("" (flatten) nil nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuity_def "topology/") (le2 formal-const-decl "(directed_complete_partial_order?[T2])" scott_continuity nil) (scott_open_sets const-decl "setofsets[T]" scott nil) (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) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T2 formal-type-decl nil scott_continuity 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) (scott_continuous? const-decl "bool" scott_continuity nil) (scott_continuous_def formula-decl nil scott_continuity nil)) shostak)) (pointwise_complete 0 (pointwise_complete-1 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" (name "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" (name "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" (inst + "F") (("1" (expand "least_upper_bound?") (("1" (split 1) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (skosimp) (("1" (typepred "r!1") (("1" (inst -14 "x!1") (("1" (typepred "lub({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst - "r!1(x!1)") (("1" (expand "F") (("1" (propax) nil nil)) nil) ("2" (inst + "r!1") nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (typepred "r!1") (("2" (expand "upper_bound?") (("2" (inst -14 "x!1") (("2" (typepred "lub({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst - "r!1(x!1)") (("1" (split -2) (("1" (expand "F") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "r!2") (("2" (skosimp) (("2" (replace -1) (("2" (inst -4 "f!1") (("2" (inst -4 "x!1") 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) ("2" (expand "scott_continuous?") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "lub_preserving?") (("2" (skosimp) (("2" (inst - "D!2") (("2" (inst - "D!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (skosimp) (("2" (lemma "lub_set_image" ("g" "F" "D" "D!2")) (("2" (inst - "D!2") (("2" (typepred "lub(image[T1, T2](F, D!2))") (("2" (typepred "lub(FX(D!2))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst - "lub(image[T1, T2](F, D!2))") (("1" (split -2) (("1" (inst -4 "lub(FX(D!2))") (("1" (split -4) (("1" (lemma "partial_order_antisymmetric" ("x" "lub(image[T1, T2](F, D!2))" "y" "lub(FX(D!2))")) (("1" (assert) nil nil)) nil) ("2" (hide 2 -1) (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "r!1") (("2" (expand "image") (("2" (skosimp) (("2" (replace -1) (("2" (inst -12 "x!1") (("2" (typepred "lub({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst - "lub(FX(D!2))") (("1" (split -2) (("1" (expand "F") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "r!2") (("2" (skosimp) (("2" (replace -1) (("2" (inst -4 "f!1(x!1)") (("2" (expand "FX") (("2" (inst + "f!1" "x!1") 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)) nil)) nil) ("2" (propax) 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" (hide 2) (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "r!1") (("2" (expand "FX" -1) (("2" (skosimp) (("2" (replace -1) (("2" (inst -3 "F(x!1)") (("1" (hide-all-but (1 -3 -13)) (("1" (inst - "x!1") (("1" (name-replace "DRL100" "lub(image[T1, T2](F, D!2))") (("1" (expand "F") (("1" (typepred "lub({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (hide -2) (("1" (expand "upper_bound?") (("1" (inst - "f!1(x!1)") (("1" (lemma "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" (inst + "f!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "image") (("2" (inst + "x!1") 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (expand "F" 1) (("2" (expand "FX") (("2" (hide -3 -7) (("2" (inst - "D!2") (("2" (inst - "D!2") (("2" (flatten) (("2" (typepred "lub({y: T2 | EXISTS (f: (D!1), x: (D!2)): y = f(x)})") (("1" (typepred "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(lub(D!2))})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst -2 "lub({y: T2 | EXISTS (f: (D!1), x: (D!2)): y = f(x)})") (("1" (split -2) (("1" (inst -4 "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(lub(D!2))})") (("1" (split -4) (("1" (lemma "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" (hide 2) (("2" (skosimp) (("2" (typepred "r!1") (("2" (skosimp) (("2" (typepred "x!1") (("2" (inst -4 "f!1(lub(D!2))") (("1" (name-replace "DRL100" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(lub(D!2))})") (("1" (replace -2) (("1" (hide-all-but (1 -1 -4)) (("1" (typepred "f!1") (("1" (expand "scott_continuous?") (("1" (flatten) (("1" (typepred "lub(D!2)") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst - "x!1") (("1" (expand "increasing?") (("1" (inst - "x!1" "lub(D!2)") (("1" (assert) (("1" (lemma "partial_order_transitive" ("x" "f!1(x!1)" "y" "f!1(lub(D!2))" "z" "DRL100")) (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "f!1") nil nil) ("3" (typepred "le1") (("3" (expand "directed_complete_partial_order?") (("3" (flatten) nil nil)) nil)) nil) ("4" (typepred "le2") (("4" (expand "directed_complete_partial_order?") (("4" (flatten) (("4" (lemma "directed_is_lub_set[T1,le1]") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -10 "lub(D!2)") (("1" (typepred "le1") (("1" (expand "directed_complete_partial_order?") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "directed_is_lub_set[T1,le1]") (("2" (inst?) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "le1") (("3" (expand "directed_complete_partial_order?") (("3" (flatten) nil nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma "directed_is_lub_set[T1,le1]") (("4" (inst?) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "r!1") (("2" (skosimp) (("2" (replace -1) (("2" (hide 2) (("2" (hide -1) (("2" (typepred "f!1") (("2" (expand "scott_continuous?") (("2" (flatten) (("2" (expand "lub_preserving?") (("2" (inst - "D!2") (("2" (lemma "lub_set_image" ("g" "f!1" "D" "D!2")) (("2" (assert) (("2" (replace -3) (("2" (expand "image") (("2" (name-replace "DRL101" "{y: T2 | EXISTS (f: (D!1), x: (D!2)): y = f(x)}") (("2" (name-replace "DRL102" "{y: T2 | EXISTS (x: (D!2)): y = f!1(x)}") (("2" (lemma "above_lub[T2,le2]") (("2" (inst - "DRL101" "DRL102") (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "above?") (("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "DRL102") (("2" (skosimp) (("2" (replace -1) (("2" (expand "DRL101") (("2" (inst + "f!1(x!2)") (("1" (rewrite "partial_order_reflexive") nil nil) ("2" (expand "DRL101") (("2" (inst + "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" (inst -8 "lub(D!2)") (("1" (typepred "le1") (("1" (expand "directed_complete_partial_order?") (("1" (flatten) nil nil)) nil)) nil) ("2" (lemma "directed_is_lub_set[T1,le1]") (("2" (inst?) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "le1") (("3" (expand "directed_complete_partial_order?") (("3" (flatten) nil nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma "directed_is_lub_set[T1,le1]") (("4" (inst?) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil) ("4" (assert) (("4" (skosimp*) (("4" (typepred "le1") (("4" (expand "directed_complete_partial_order?") (("4" (flatten) nil nil)) nil)) nil)) nil)) nil) ("5" (propax) nil nil)) nil) ("2" (skosimp) (("2" (inst - "D!2") (("2" (flatten) (("2" (lemma "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" (skosimp*) (("3" (typepred "le2") (("3" (expand "directed_complete_partial_order?") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1 -5) (("2" (skosimp) (("2" (typepred "D!2") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (split 2) (("1" (skosimp*) (("1" (expand "FX") (("1" (inst - "x!2(x!1)") (("1" (inst + "x!2" "x!1") nil nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (expand "directed?") (("2" (skosimp*) (("2" (expand "FX") (("2" (skosimp*) (("2" (replace -1) (("2" (replace -2) (("2" (typepred "f!1") (("2" (typepred "f!2") (("2" (inst -12 "f!1" "f!2") (("2" (assert) (("2" (expand "scott_continuous?") (("2" (flatten) (("2" (hide-all-but (1 -1 -3 -4 -6 -9 -14)) (("2" (skosimp) (("2" (expand "directed?") (("2" (inst - "x!2" "x!3") (("2" (assert) (("2" (skosimp) (("2" (expand "increasing?") (("2" (inst - "x!3" "z!2") (("2" (inst - "x!2" "z!2") (("2" (assert) (("2" (inst - "z!2") (("2" (inst - "z!2") (("2" (lemma "partial_order_transitive" ("z" "z!1(z!2)")) (("2" (inst-cp - "f!1(x!2)" "f!1(z!2)") (("2" (inst - "f!2(x!3)" "f!2(z!2)") (("2" (assert) (("2" (inst + "z!1(z!2)") (("1" (assert) nil nil) ("2" (expand "FX") (("2" (inst + "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" (typepred "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" (inst-cp - "x!1") (("2" (inst - "y!1") (("2" (typepred "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})") (("1" (typepred "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(y!1)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst -4 "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(y!1)})") (("1" (split -4) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "r!1") (("2" (skosimp) (("2" (replace -1) (("2" (inst -2 "f!1(y!1)") (("1" (typepred "f!1") (("1" (expand "scott_continuous?") (("1" (flatten) (("1" (expand "increasing?") (("1" (inst - "x!1" "y!1") (("1" (assert) (("1" (lemma "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" (inst + "f!1") 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)) 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" (inst - "{y: T2 | EXISTS (f: (D!1)): y = f(x!1)}") (("2" (hide 2 -1) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp) (("1" (expand "member") (("1" (inst - "x!2(x!1)") (("1" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "directed?") (("2" (skosimp*) (("2" (replace -1) (("2" (replace -2) (("2" (typepred "f!1") (("2" (typepred "f!2") (("2" (inst - "f!1" "f!2") (("2" (assert) (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (inst + "z!1(x!1)") (("1" (assert) nil nil) ("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) ("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) ((directed_complete? const-decl "bool" directed_orders "orders/") (le2 formal-const-decl "(directed_complete_partial_order?[T2])" scott_continuity nil) (directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (pointwise const-decl "bool" pointwise_orders "orders/") (directed? const-decl "bool" directed_orders "orders/") (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (scott_continuous? const-decl "bool" scott_continuity nil) (T2 formal-type-decl nil scott_continuity 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) (least_bounded_above? const-decl "bool" bounded_orders "orders/") (z!1 skolem-const-decl "(D!1)" scott_continuity nil) (x!2 skolem-const-decl "(scott_continuous?)" scott_continuity nil) (x!1 skolem-const-decl "T1" scott_continuity nil) (least_upper_bound? const-decl "bool" bounded_orders "orders/") (lub const-decl "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" bounded_order_props "orders/") (y!1 skolem-const-decl "T1" scott_continuity nil) (f!1 skolem-const-decl "(D!1)" scott_continuity nil) (directed_is_lub_set judgement-tcc nil directed_order_props "orders/") (directed? const-decl "bool" directed_order_props "orders/") (directed type-eq-decl nil directed_order_props "orders/") (empty? const-decl "bool" sets nil) (D!2 skolem-const-decl "directed[T1, le1]" scott_continuity nil) (x!1 skolem-const-decl "T1" scott_continuity nil) (x!2 skolem-const-decl "(scott_continuous?)" scott_continuity nil) (z!1 skolem-const-decl "(D!1)" scott_continuity nil) (z!2 skolem-const-decl "(D!2)" scott_continuity nil) (member const-decl "bool" sets nil) (f!1 skolem-const-decl "(D!1)" scott_continuity nil) (above_lub formula-decl nil bounded_order_props "orders/") (above? const-decl "bool" bounded_order_props "orders/") (DRL101 skolem-const-decl "[T2 -> boolean]" scott_continuity nil) (partial_order_reflexive formula-decl nil partial_order_props "orders/") (x!2 skolem-const-decl "(D!2)" scott_continuity nil) (f!1 skolem-const-decl "(D!1)" scott_continuity nil) (DRL102 skolem-const-decl "[T2 -> boolean]" scott_continuity nil) (D!2 skolem-const-decl "directed[T1, le1]" scott_continuity nil) (image const-decl "set[R]" function_image nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (x!1 skolem-const-decl "T1" scott_continuity nil) (r!1 skolem-const-decl "(D!1)" scott_continuity nil) (F skolem-const-decl "[x: T1 -> {x_1 | bounded_orders[T2].least_upper_bound? (x_1, {y: T2 | EXISTS (f: (D!1)): y = f(x)}, le2)}]" scott_continuity nil) (D!1 skolem-const-decl "(directed?(LAMBDA (s: [(scott_continuous?), (scott_continuous?)]): pointwise(le2)(s)))" scott_continuity nil) (lub_preserving? const-decl "bool" scott_continuity nil) (partial_order_antisymmetric formula-decl nil partial_order_props "orders/") (FX skolem-const-decl "[directed[T1, le1] -> [T2 -> boolean]]" scott_continuity nil) (D!2 skolem-const-decl "directed[T1, le1]" scott_continuity nil) (f!1 skolem-const-decl "(D!1)" scott_continuity nil) (x!1 skolem-const-decl "(D!2)" scott_continuity nil) (x!1 skolem-const-decl "(D!2)" scott_continuity nil) (f!1 skolem-const-decl "(D!1)" scott_continuity nil) (partial_order_transitive formula-decl nil partial_order_props "orders/") (AND const-decl "[bool, bool -> bool]" booleans nil) (lub_set_image formula-decl nil scott_continuity nil) (increasing? const-decl "bool" fun_preds_partial nil) (le1 formal-const-decl "(directed_complete_partial_order?[T1])" scott_continuity nil) (= const-decl "[T, T -> boolean]" equalities nil) (lub_set? const-decl "bool" bounded_order_props "orders/") (restrict const-decl "R" restrict nil)) shostak)) (scott_continuous_dcpo 0 (scott_continuous_dcpo-1 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" (skosimp*) (("1" (inst?) nil nil)) nil)) nil) ("2" (expand "transitive?") (("2" (skosimp*) (("2" (inst -1 "x!2") (("2" (inst - "x!2") (("2" (assert) (("2" (inst - "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" (apply-extensionality 1 :hide? t) (("2" (inst - "x!2") (("2" (inst - "x!2") (("2" (inst - "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_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (pointwise_complete formula-decl nil scott_continuity nil)) shostak)) (IMP_scott_TCC1 0 (IMP_scott_TCC1-1 nil 3352749145 ("" (lemma "scott_continuous_dcpo") (("" (propax) nil nil)) nil) ((scott_continuous_dcpo formula-decl nil scott_continuity nil)) nil)))
¤ 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.229Bemerkung: (vorverarbeitet am 2026-05-05) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26