| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/while/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 177 kB |
|
Quelle Cont.prfSprache: Lisp |
|||||||||||||||
|
(Cont (sq_le_def 0 (sq_le_def-1 nil 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" (prop) (("2" (replace -2 1 rl) (("2" (lemma "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) ((sq_le const-decl "bool" Cont nil) (member const-decl "bool" sets nil) (down_up formula-decl nil lift_props "orders/") (extend const-decl "R" extend nil) (graph const-decl "bool" functions nil) (V formal-nonempty-type-decl nil Cont nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (State nonempty-type-eq-decl nil State nil) (Cont nonempty-type-eq-decl nil Cont nil) (lift type-decl nil lift_adt nil) (up_down formula-decl nil lift_props "orders/") (LPartFun_to_SPartFun const-decl "SubsetPartialFunction" PartialFunctionDefinitions nil) (graph const-decl "set[[X, Y]]" partial_function_props "scott/") (subset? const-decl "bool" sets nil)) shostak)) (partial_order_sq_le 0 (partial_order_sq_le-1 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) ((preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (subset_antisymmetric formula-decl nil sets_lemmas nil) (graph_eq formula-decl nil partial_function_props "scott/") (transitive? const-decl "bool" relations nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (reflexive? const-decl "bool" relations nil) (sq_le_def formula-decl nil Cont nil) (V formal-nonempty-type-decl nil Cont nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (State nonempty-type-eq-decl nil State nil) (lift type-decl nil lift_adt nil) (Cont nonempty-type-eq-decl nil Cont nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (graph const-decl "set[[X, Y]]" partial_function_props "scott/") (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (subset_reflexive formula-decl nil sets_lemmas nil) (partial_order? const-decl "bool" orders nil)) shostak)) (lub_graph_TCC1 0 (lub_graph_TCC1-1 nil 3353058858 ("" (subtype-tcc) nil nil) ((member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil)) nil)) (lub_graph_TCC2 0 (lub_graph_TCC2-1 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" (hide -3 -4) (("2" (expand "graph") (("2" (expand "extend") (("2" (expand "LPartFun_to_SPartFun") (("2" (expand "graph") (("2" (prop) (("2" (expand "directed?") (("2" (inst - "x!2" "x!3") (("2" (assert) (("2" (skosimp) (("2" (typepred "z!1") (("2" (expand "sq_le") (("2" (inst - "x!1" "y2!1") (("2" (inst - "x!1" "y1!1") (("2" (lemma "up_down" ("y" "x!2(x!1)")) (("2" (lemma "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) ((graph? const-decl "bool" partial_function_props "scott/") (Union const-decl "set" sets nil) (graph const-decl "set[[X, Y]]" partial_function_props "scott/") (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions nil) (= const-decl "[T, T -> boolean]" equalities nil) (emptyset const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (image const-decl "set[R]" function_image nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[Cont]" Cont nil) (Cont nonempty-type-eq-decl nil Cont nil) (lift type-decl nil lift_adt nil) (State nonempty-type-eq-decl nil State nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (V formal-nonempty-type-decl nil Cont nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (LPartFun_to_SPartFun const-decl "SubsetPartialFunction" PartialFunctionDefinitions nil) (sq_le const-decl "bool" Cont nil) (up_down formula-decl nil lift_props "orders/") (directed? const-decl "bool" directed_orders "orders/") (graph const-decl "bool" functions nil) (extend const-decl "R" extend nil)) nil)) (lub_graph 0 (lub_graph-1 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" (case-replace "{y: State | Union(image(graph, D!1))(s1!1, y)} = singleton(s2!1)") (("1" (rewrite "choose_singleton") nil nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "singleton") (("2" (case-replace "x!1=s2!1") (("1" (typepred "r!1") (("1" (expand "Union") (("1" (inst + "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" (inst + "r!1") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "image") (("2" (skosimp) (("2" (typepred "x!2") (("2" (replace -2) (("2" (hide -2) (("2" (typepred "r!1") (("2" (expand "directed?") (("2" (inst - "x!2" "r!1") (("2" (assert) (("2" (skosimp) (("2" (expand "graph") (("2" (expand "extend") (("2" (prop) (("2" (expand "graph") (("2" (expand "LPartFun_to_SPartFun") (("2" (replace -2 * rl) (("2" (inst - "s1!1" "x!1") (("2" (inst - "s1!1" "s2!1") (("2" (assert) (("2" (split -7) (("1" (lemma "down_equal" ("y1" "up(x!1)" "y2" "up(s2!1)")) (("1" (assert) nil nil)) nil) ("2" (replace -2 1 rl) (("2" (lemma "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" (skosimp) (("2" (expand "member") (("2" (inst - "s2!1") (("2" (expand "Union") (("2" (inst + "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" (inst + "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" (skosimp*) (("2" (expand "Union" -1) (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "image" -1) (("2" (skosimp) (("2" (replace -1) (("2" (typepred "x!2") (("2" (hide -2) (("2" (inst -5 "x!2") (("2" (inst -5 "s1!1" "x!1") (("2" (expand "graph" -2) (("2" (expand "extend") (("2" (expand "LPartFun_to_SPartFun") (("2" (prop) (("1" (expand "graph" -3) (("1" (case-replace "{y:State|Union(image(graph,D!1))(s1!1,y)} =singleton(x!1)") (("1" (rewrite "choose_singleton") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "singleton") (("2" (case-replace "x!3 = x!1") (("1" (expand "Union") (("1" (inst + "graph(x!2)") (("1" (expand "graph") (("1" (expand "extend") (("1" (expand "LPartFun_to_SPartFun") (("1" (expand "graph") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "image") (("2" (inst + "x!2") nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!2") (("2" (expand "image") (("2" (skosimp) (("2" (typepred "x!4") (("2" (replace -2) (("2" (hide -2) (("2" (expand "graph") (("2" (expand "extend") (("2" (expand "LPartFun_to_SPartFun") (("2" (expand "graph") (("2" (prop) (("2" (hide-all-but (-1 -2 -3 -5 -6 -7 -10 1)) (("2" (expand "directed?") (("2" (inst - "x!2" "x!4") (("2" (assert) (("2" (skosimp) (("2" (inst - "s1!1" "x!1") (("2" (inst - "s1!1" "x!3") (("2" (lemma "up_down" ("y" "x!4(s1!1)")) (("2" (lemma "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" (lemma "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" (case-replace "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" (skosimp) (("2" (expand "member") (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (typepred "x!3") (("2" (inst - "x!3") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((V formal-nonempty-type-decl nil Cont nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (State nonempty-type-eq-decl nil State nil) (lift type-decl nil lift_adt nil) (Cont nonempty-type-eq-decl nil Cont nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (least_upper_bound? const-decl "bool" bounded_orders "orders/") (x!2 skolem-const-decl "(D!1)" Cont nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (sq_le const-decl "bool" Cont nil) (from_graph const-decl "LiftPartialFunction" partial_function_props "scott/") (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (Union const-decl "set" sets nil) (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions nil) (image const-decl "set[R]" function_image nil) (graph const-decl "set[[X, Y]]" partial_function_props "scott/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (choose_singleton formula-decl nil sets_lemmas nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (LPartFun_to_SPartFun const-decl "SubsetPartialFunction" PartialFunctionDefinitions nil) (down_up formula-decl nil lift_props "orders/") (graph const-decl "bool" functions nil) (extend const-decl "R" extend nil) (r!1 skolem-const-decl "(D!1)" Cont nil) (D!1 skolem-const-decl "set[Cont]" Cont nil) (NOT const-decl "[bool -> bool]" booleans nil) (up adt-constructor-decl "[T -> (up?)]" lift_adt nil) (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (down_equal formula-decl nil lift_props "orders/") (up_down formula-decl nil lift_props "orders/") (directed? const-decl "bool" directed_orders "orders/") (emptyset_is_empty? formula-decl nil sets_lemmas nil) (finite_emptyset name-judgement "finite_set[Cont]" Cont nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (bottom adt-constructor-decl "(bottom?)" lift_adt nil) (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (graph? const-decl "bool" partial_function_props "scott/")) shostak)) (sq_le_dcpo 0 (sq_le_dcpo-1 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" (split) (("1" (skosimp) (("1" (skosimp) (("1" (lift-if 1) (("1" (assert) (("1" (prop) (("1" (typepred "r!1") (("1" (lemma "down_equal" ("y1" "up(choose({y: State | Union(image(graph, D!1))(s1!1, y)}))" "y2" "up(s2!1)")) (("1" (split -1) (("1" (flatten -1) (("1" (hide -2) (("1" (rewrite "down_up" -1) (("1" (rewrite "down_up" -1) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (lemma "choose_singleton" ("x" "s2!1")) (("2" (expand "singleton") (("2" (case-replace "{y: State | Union(image(graph, D!1))(s1!1, y)} = {y: State | y = s2!1}") (("2" (hide -1 2) (("2" (apply-extensionality 1 :hide? t) (("2" (case-replace "x!1=s2!1") (("1" (expand "Union") (("1" (inst + "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" (inst + "r!1") nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "image") (("2" (skosimp) (("2" (typepred "x!2") (("2" (replace -2) (("2" (expand "graph") (("2" (expand "extend") (("2" (expand "LPartFun_to_SPartFun") (("2" (hide -2) (("2" (expand "graph") (("2" (prop) (("2" (typepred "D!1") (("2" (expand "directed?") (("2" (expand "sq_le") (("2" (inst - "x!2" "r!1") (("2" (assert) (("2" (skosimp) (("2" (typepred "z!1") (("2" (inst - "s1!1" "x!1") (("2" (lemma "up_down" ("y" "x!2(s1!1)")) (("2" (assert) (("2" (inst - "s1!1" "s2!1") (("2" (assert) (("2" (lemma "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" (typepred "r!1") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "s2!1") (("2" (expand "Union") (("2" (inst + "graph(r!1)") (("1" (expand "graph") (("1" (expand "extend") (("1" (expand "LPartFun_to_SPartFun") (("1" (expand "graph") (("1" (replace -2) (("1" (rewrite "down_up") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "image") (("2" (inst + "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lift-if -2) (("2" (assert) (("2" (prop) (("2" (hide -5) (("2" (hide -5) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "image") (("2" (skosimp) (("2" (typepred "x!2") (("2" (inst -5 "x!2") (("2" (replace -2) (("2" (hide -2) (("2" (case-replace "{y: State | EXISTS (a: (image(graph, D!1))): a(s1!1, y)} = singleton(x!1)") (("1" (hide -1) (("1" (rewrite "choose_singleton") (("1" (lemma "down_equal" ("y1" "up(x!1)" "y2" "up(s2!1)")) (("1" (assert) (("1" (replace -1) (("1" (inst - "s1!1" "s2!1") (("1" (expand "graph") (("1" (expand "extend") (("1" (expand "LPartFun_to_SPartFun") (("1" (expand "graph") (("1" (prop) (("1" (replace -2 1 rl) (("1" (lemma "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" (hide 2) (("2" (expand "graph?") (("2" (apply-extensionality 1 :hide? t) (("2" (expand "singleton") (("2" (case-replace "x!3=x!1") (("1" (inst + "graph(x!2)") (("1" (expand "image") (("1" (inst + "x!2") nil nil)) nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (typepred "a!2") (("2" (expand "image") (("2" (skosimp) (("2" (replace -1) (("2" (hide -1) (("2" (typepred "x!4") (("2" (hide -5 -6) (("2" (inst - "s1!1" "x!3" "x!1") (("2" (split -5) (("1" (propax) nil nil) ("2" (inst + "graph(x!4)") (("2" (expand "image") (("2" (inst + "x!4") nil nil)) nil)) nil) ("3" (inst + "graph(x!2)") (("3" (expand "image") (("3" (inst + "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" (skosimp) (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp*) (("2" (typepred "a!1") (("2" (typepred "a!2") (("2" (skosimp*) (("2" (replace -1) (("2" (replace -2) (("2" (hide -1 -2) (("2" (expand "graph") (("2" (expand "extend") (("2" (expand "LPartFun_to_SPartFun") (("2" (expand "graph") (("2" (prop) (("2" (typepred "x!2") (("2" (typepred "x!3") (("2" (inst - "x!2" "x!3") (("2" (assert) (("2" (skosimp) (("2" (expand "sq_le") (("2" (inst - "x!1" "y2!1") (("2" (inst - "x!1" "y1!1") (("2" (assert) (("2" (lemma "up_down" ("y" "x!3(x!1)")) (("2" (lemma "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) ((partial_order_sq_le judgement-tcc nil Cont nil) (directed_complete? const-decl "bool" directed_orders "orders/") (least_bounded_above? const-decl "bool" bounded_orders "orders/") (graph? const-decl "bool" partial_function_props "scott/") (least_upper_bound? const-decl "bool" bounded_orders "orders/") (x!2 skolem-const-decl "(D!1)" Cont nil) (x!4 skolem-const-decl "(D!1)" Cont nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (singleton? const-decl "bool" sets nil) (down_equal formula-decl nil lift_props "orders/") (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" lift_adt nil) (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (up adt-constructor-decl "[T -> (up?)]" lift_adt nil) (choose const-decl "(p)" sets nil) (down_up formula-decl nil lift_props "orders/") (choose_singleton formula-decl nil sets_lemmas nil) (up_down formula-decl nil lift_props "orders/") (LPartFun_to_SPartFun const-decl "SubsetPartialFunction" PartialFunctionDefinitions nil) (graph const-decl "bool" functions nil) (extend const-decl "R" extend nil) (r!1 skolem-const-decl "(D!1)" Cont nil) (D!1 skolem-const-decl "(directed?(sq_le))" Cont nil) (singleton const-decl "(singleton?)" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (from_graph const-decl "LiftPartialFunction" partial_function_props "scott/") (G skolem-const-decl "set[[State[V], State[V]]]" Cont nil) (V formal-nonempty-type-decl nil Cont nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (State nonempty-type-eq-decl nil State nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (Union const-decl "set" sets nil) (lift type-decl nil lift_adt nil) (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions nil) (image const-decl "set[R]" function_image nil) (graph const-decl "set[[X, Y]]" partial_function_props "scott/") (Cont nonempty-type-eq-decl nil Cont nil) (nonempty? const-decl "bool" sets nil) (pred type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (directed? const-decl "bool" directed_orders "orders/") (sq_le const-decl "bool" Cont nil) (directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (partial_order_sq_le name-judgement "(partial_order?[Cont])" Cont nil)) shostak)) (sq_le_pdcpo 0 (sq_le_pdcpo-1 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) ((sq_le_dcpo judgement-tcc nil Cont nil) (fullset const-decl "set" sets nil) (sq_le const-decl "bool" Cont nil) (V formal-nonempty-type-decl nil Cont nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (State nonempty-type-eq-decl nil State nil) (lift type-decl nil lift_adt nil) (Cont nonempty-type-eq-decl nil Cont nil) (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (bottom adt-constructor-decl "(bottom?)" lift_adt nil) (lower_bound? const-decl "bool" bounded_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (has_least? const-decl "bool" minmax_orders "orders/") (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (partial_order_sq_le name-judgement "(partial_order?[Cont])" Cont nil) (sq_le_dcpo name-judgement "(directed_complete_partial_order?[Cont])" Cont nil)) shostak)) (sq_le_bottom 0 (sq_le_bottom-1 nil 3353817335 ("" (expand "sq_le") (("" (propax) nil nil)) nil) ((sq_le const-decl "bool" Cont nil)) shostak)) (sq_le_least 0 (sq_le_least-1 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) ((fullset const-decl "set" sets nil) (sq_le_bottom formula-decl nil Cont nil) (V formal-nonempty-type-decl nil Cont nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (State nonempty-type-eq-decl nil State nil) (lift type-decl nil lift_adt nil) (Cont nonempty-type-eq-decl nil Cont nil) (bool nonempty-type-eq-decl nil booleans nil) (TRUE const-decl "bool" booleans nil) (lower_bound? const-decl "bool" bounded_orders "orders/") (least? const-decl "bool" minmax_orders "orders/")) shostak)) (sq_le_conditional 0 (sq_le_conditional-1 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) ((sq_le const-decl "bool" Cont nil) (V formal-nonempty-type-decl nil Cont nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (State nonempty-type-eq-decl nil State nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (conditional const-decl "Cont" Cont nil)) shostak)) (apply_continuous 0 (apply_continuous-1 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" (inst - "F(lub(D!1))" "lub(image(F, D!1))") (("1" (assert) (("1" (hide 2 -4) (("1" (expand "F" 1) (("1" (typepred "lub(D!1)") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (case "FORALL (r: Cont): (FORALL (r_1: (D!1)): (sq_le)(r_1 o G, r)) => (sq_le)(lub(D!1) o G, r)") (("1" (inst - "lub(image(LAMBDA c: c o G, D!1))") (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "r!1") (("2" (replace -8 *) (("2" (typepred "lub(image(F, D!1))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?") (("2" (inst - "r!1 o G") (("2" (expand "image") (("2" (inst + "r!1") (("2" (expand "F") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -8 1)) (("2" (skosimp) (("2" (name-replace "DRL1" "lub(D!1)") (("2" (expand "sq_le") (("2" (skosimp) (("2" (expand "o" -2) (("2" (case "EXISTS (c:(D!1)): (c o G)(s1!1) = up(s2!1)") (("1" (skosimp) (("1" (inst - "c!1") (("1" (inst - "s1!1" "s2!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "o ") (("2" (case "bottom?(G(s1!1))") (("1" (assert) nil nil) ("2" (name "X" "{c:(D!1)| c(down(G(s1!1))) = up(s2!1)}") (("1" (case "nonempty?(X)") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp) (("1" (expand "member") (("1" (expand "X") (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lift-if -3) (("2" (assert) (("2" (expand "DRL1") (("2" (hide -1 -2 -4 -5) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (typepred "lub(D!1)") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (case "FORALL (s: State, r1, r2: (D!1)): (NOT bottom?(r1(s)) & NOT bottom?(r2(s))) => r1(s) = r2(s)") (("1" (name-replace "S" "down(G(s1!1))") (("1" (case "forall (r:(D!1)): r(S) = bottom[State]") (("1" (inst -4 "lambda s: if s = S then bottom[State] else lub(D!1)(s) endif") (("1" (split -4) (("1" (expand "sq_le") (("1" (inst - "S" "s2!1") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "upper_bound?") (("2" (skosimp) (("2" (expand "sq_le") (("2" (skosimp) (("2" (typepred "r!2") (("2" (inst -3 "r!2") (("2" (assert) (("2" (case-replace "s1!2=S") (("1" (assert) nil nil) ("2" (assert) (("2" (inst -5 "r!2") (("2" (inst -5 "s1!2" "s2!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "r!2") (("2" (inst -4 "lambda s: if s = S then r!2(s) else lub(D!1)(s) endif") (("2" (split -4) (("1" (expand "sq_le" -1) (("1" (inst - "S" "s2!1") (("1" (assert) (("1" (inst -5 "r!2") (("1" (expand "X") (("1" (expand "S") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "r!3") (("2" (expand "sq_le" 1) (("2" (skosimp) (("2" (case-replace "s1!2 = S") (("1" (inst - "S" "r!2" "r!3") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "sq_le" -5) (("2" (inst -5 "r!3") (("2" (inst -5 "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" (hide-all-but 1) (("2" (skosimp) (("2" (typepred "r1!1") (("2" (typepred "r2!1") (("2" (typepred "D!1") (("2" (expand "directed?") (("2" (expand "directed?") (("2" (inst - "r1!1" "r2!1") (("2" (assert) (("2" (skosimp) (("2" (expand "sq_le") (("2" (inst - "s!1" "down(r1!1(s!1))") (("2" (inst - "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" (skosimp) (("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" (case-replace "bottom?(G(s1!1))") (("2" (assert) (("2" (inst - "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) ((scott_continuous? const-decl "bool" scott_continuity "scott/") (O const-decl "LiftPartialFunction[X, Z]" PartialFunctionComposition nil) (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions nil) (increasing? const-decl "bool" fun_preds_partial "scott/") (sq_le const-decl "bool" Cont nil) (bool nonempty-type-eq-decl nil booleans nil) (partial_order_sq_le name-judgement "(partial_order?[Cont])" Cont nil) (sq_le_dcpo name-judgement "(directed_complete_partial_order?[Cont])" Cont nil) (sq_le_pdcpo name-judgement "(pointed_directed_complete_partial_order?[Cont])" Cont nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (partial_order? const-decl "bool" orders 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/") (least_upper_bound? const-decl "bool" bounded_orders "orders/") (lub_set? const-decl "bool" bounded_order_props "orders/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (G skolem-const-decl "Cont" Cont nil) (r!1 skolem-const-decl "(D!1)" Cont nil) (D!1 skolem-const-decl "directed[Cont, (sq_le)]" Cont nil) (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (X skolem-const-decl "[(D!1) -> boolean]" Cont nil) (DRL1 skolem-const-decl "{x | bounded_orders[Cont].least_upper_bound?(x, D!1, (sq_le))}" Cont nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bottom adt-constructor-decl "(bottom?)" lift_adt nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (S skolem-const-decl "State[V]" Cont nil) (up_down formula-decl nil lift_props "orders/") (directed? const-decl "bool" directed_orders "orders/") (down adt-accessor-decl "[(up?) -> T]" lift_adt nil) (up adt-constructor-decl "[T -> (up?)]" lift_adt nil) (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (F skolem-const-decl "[Cont -> LiftPartialFunction[State[V], State[V]]]" Cont nil) (fullset_is_clopen name-judgement "clopen[Cont, scott_open_sets]" Cont nil) (pointwise_preserves_partial_order application-judgement "(partial_order?[[Cont -> Cont]])" Cont nil) (antisymmetric? const-decl "bool" relations 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) (lub_image formula-decl nil scott_continuity "scott/") (lub_preserving? const-decl "bool" scott_continuity "scott/") (= const-decl "[T, T -> boolean]" equalities nil) (Cont nonempty-type-eq-decl nil Cont nil) (lift type-decl nil lift_adt nil) (State nonempty-type-eq-decl nil State nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (V formal-nonempty-type-decl nil Cont nil)) shostak)))
¤ Dauer der Verarbeitung: 0.161 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26