|
(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
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.67 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
