|
(sum_orders
(sum_preserves_reflexive 0
(sum_preserves_reflexive-1 nil 3353304649
("" (judgement-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T1 formal-type-decl nil sum_orders nil)
(PRED type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil sum_orders nil)
(inr? adt-recognizer-decl "[union -> boolean]" union_adt nil)
(right adt-accessor-decl "[(inr?) -> T2]" union_adt nil)
(union type-decl nil union_adt nil)
(inl? adt-recognizer-decl "[union -> boolean]" union_adt nil)
(left adt-accessor-decl "[(inl?) -> T1]" union_adt nil)
(+ const-decl "bool" sum_orders nil)
(reflexive? const-decl "bool" relations nil))
nil))
(sum_preserves_transitive 0
(sum_preserves_transitive-1 nil 3353304649
("" (skosimp)
(("" (typepred "r2!1")
(("" (typepred "r1!1")
(("" (expand "transitive?")
(("" (skosimp)
(("" (expand "+")
(("" (assert)
(("" (flatten)
(("" (case-replace "inl?(x!1)")
(("1" (assert)
(("1" (flatten)
(("1" (assert)
(("1" (flatten)
(("1"
(inst -2 "left(x!1)" "left(y!1)"
"left(z!1)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (flatten)
(("2" (assert)
(("2" (flatten)
(("2"
(inst -2 "right(x!1)" "right(y!1)"
"right(z!1)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil sum_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(+ const-decl "bool" sum_orders nil)
(right adt-accessor-decl "[(inr?) -> T2]" union_adt nil)
(inr? adt-recognizer-decl "[union -> boolean]" union_adt nil)
(left adt-accessor-decl "[(inl?) -> T1]" union_adt nil)
(union type-decl nil union_adt nil)
(inl? adt-recognizer-decl "[union -> boolean]" union_adt nil)
(T1 formal-type-decl nil sum_orders nil))
nil))
(sum_preserves_antisymmetric 0
(sum_preserves_antisymmetric-1 nil 3353304649
("" (skosimp)
(("" (typepred "r2!1")
(("" (typepred "r1!1")
(("" (expand "antisymmetric?")
(("" (skosimp)
(("" (expand "+")
(("" (case-replace "inl?(x!1)")
(("1" (assert)
(("1" (flatten)
(("1" (inst -2 "left(x!1)" "left(y!1)")
(("1" (assert)
(("1" (decompose-equality) nil nil)) nil))
nil))
nil))
nil)
("2" (assert)
(("2" (flatten)
(("2" (inst -2 "right(x!1)" "right(y!1)")
(("2" (assert)
(("2" (case "inr?(x!1)")
(("1" (assert)
(("1" (grind)
(("1"
(hide -2 -5)
(("1" (decompose-equality 1) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil sum_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(+ const-decl "bool" sum_orders nil)
(right adt-accessor-decl "[(inr?) -> T2]" union_adt nil)
(inr? adt-recognizer-decl "[union -> boolean]" union_adt nil)
(union_inr_extensionality formula-decl nil union_adt nil)
(left adt-accessor-decl "[(inl?) -> T1]" union_adt nil)
(union_inl_extensionality formula-decl nil union_adt nil)
(union type-decl nil union_adt nil)
(inl? adt-recognizer-decl "[union -> boolean]" union_adt nil)
(T1 formal-type-decl nil sum_orders nil))
nil))
(sum_preserves_preorder 0
(sum_preserves_preorder-1 nil 3353304649 ("" (judgement-tcc) nil nil)
((sum_preserves_transitive application-judgement
"(transitive?[union[T1, T2]])" sum_orders nil)
(sum_preserves_reflexive application-judgement
"(reflexive?[union[T1, T2]])" sum_orders nil)
(preorder? const-decl "bool" orders nil))
nil))
(sum_preserves_partial_order 0
(sum_preserves_partial_order-1 nil 3353304649
("" (judgement-tcc) nil nil)
((sum_preserves_antisymmetric application-judgement
"(antisymmetric?[union[T1, T2]])" sum_orders nil)
(sum_preserves_preorder application-judgement
"(preorder?[union[T1, T2]])" sum_orders nil)
(partial_order? const-decl "bool" orders nil))
nil))
(sum_preserves_directed_complete 0
(sum_preserves_directed_complete-1 nil 3353304649
("" (skosimp)
(("" (typepred "r2!1")
(("" (typepred "r1!1")
(("" (expand "directed_complete?")
(("" (skosimp)
(("" (typepred "D!1")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (skosimp)
(("" (expand "member")
(("" (case "inl?(x!1)")
(("1" (name "LD" "{x:T1 | D!1(inl(x))}")
(("1" (hide -7 -8)
(("1"
(case "D!1=image[T1,union[T1,T2]](inl,LD)")
(("1"
(inst - "LD")
(("1"
(expand "least_bounded_above?")
(("1"
(skosimp)
(("1"
(inst + "inl(t!1)")
(("1"
(expand "least_upper_bound?")
(("1"
(expand "upper_bound?")
(("1"
(flatten)
(("1"
(split)
(("1"
(skosimp)
(("1"
(expand "+")
(("1"
(typepred "r!1")
(("1"
(replace -2 -1)
(("1"
(expand
"image")
(("1"
(skosimp)
(("1"
(assert)
(("1"
(inst
-8
"x!2")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(case-replace
"left[T1,T2](inl(x!2)) =x!2")
(("1"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand "+")
(("2"
(case-replace
"inl?(r!1)")
(("1"
(inst
-10
"left(r!1)")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(typepred
"r!2")
(("1"
(expand
"LD"
-1)
(("1"
(inst
-3
"inl(r!2)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case-replace
"inr?(r!1)")
(("1"
(inst
-
"x!1")
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(split)
(("1"
(expand "nonempty?")
(("1"
(expand "empty?")
(("1"
(inst - "left(x!1)")
(("1"
(expand "member")
(("1"
(replace -1 -4)
(("1"
(expand "image")
(("1"
(skosimp)
(("1"
(typepred "x!2")
(("1"
(replace -5)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "directed?")
(("2"
(skosimp)
(("2"
(inst
-
"inl(x!2)"
"inl(y!1)")
(("2"
(assert)
(("2"
(expand "LD" (-1 -2))
(("2"
(assert)
(("2"
(skosimp)
(("2"
(expand "+")
(("2"
(flatten)
(("2"
(typepred
"z!1")
(("2"
(replace
-4
-1)
(("2"
(expand
"image")
(("2"
(skosimp)
(("2"
(inst
+
"x!3")
(("2"
(assert)
(("2"
(replace
-1)
(("2"
(assert)
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"
(apply-extensionality 1 :hide? t)
(("2"
(case-replace "D!1(x!2)")
(("1"
(expand "image")
(("1"
(case "inl?(x!2)")
(("1"
(inst + "left(x!2)")
(("1"
(assert)
(("1"
(hide-all-but 1)
(("1"
(grind)
(("1"
(decompose-equality)
nil
nil))
nil))
nil))
nil)
("2"
(expand "LD")
(("2"
(hide-all-but (-1 -2 1))
(("2"
(grind)
(("2"
(case-replace
"inl(left[T1, T2](x!2)) = x!2")
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "inr?(x!2)")
(("1"
(expand "directed?")
(("1"
(inst - "x!1" "x!2")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(expand "+")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand "image")
(("2"
(skosimp)
(("2"
(typepred "x!3")
(("2"
(expand "LD")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "inr?(x!1)")
(("1" (hide 1 -4 -5)
(("1" (name "RD" "{x:T2| D!1(inr(x))}")
(("1"
(case
"D!1=image[T2, union[T1, T2]](inr,RD)")
(("1"
(inst - "RD")
(("1"
(expand "least_bounded_above?")
(("1"
(skosimp)
(("1"
(inst + "inr(t!1)")
(("1"
(expand "least_upper_bound?")
(("1"
(flatten)
(("1"
(split)
(("1"
(expand "upper_bound?")
(("1"
(skosimp)
(("1"
(expand "+")
(("1"
(typepred "r!1")
(("1"
(hide -6 -9)
(("1"
(replace
-2
-1)
(("1"
(expand
"image")
(("1"
(skosimp)
(("1"
(typepred
"x!2")
(("1"
(inst
-8
"x!2")
(("1"
(replace
-2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand "+")
(("2"
(expand
"upper_bound?")
(("2"
(assert)
(("2"
(case-replace
"inr?(r!1)")
(("1"
(inst
-10
"right(r!1)")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(typepred
"r!2")
(("1"
(expand
"RD")
(("1"
(inst
-3
"inr(r!2)")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case
"inl?(r!1)")
(("1"
(assert)
(("1"
(inst
-2
"x!1")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(split)
(("1"
(expand "nonempty?")
(("1"
(expand "empty?")
(("1"
(inst - "right(x!1)")
(("1"
(expand "member")
(("1"
(expand "RD")
(("1"
(case-replace
"inr(right(x!1))=x!1")
(("1"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "directed?")
(("2"
(skosimp)
(("2"
(expand "RD")
(("2"
(inst
-7
"inr(x!2)"
"inr(y!1)")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(expand "+")
(("2"
(flatten)
(("2"
(inst
+
"right(z!1)")
(("1"
(assert)
nil
nil)
("2"
(expand "RD")
(("2"
(case-replace
"inr(right[T1, T2](z!1))=z!1")
(("1"
(assert)
nil
nil)
("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(apply-extensionality 1 :hide? t)
(("2"
(case-replace "D!1(x!2)")
(("1"
(expand "image")
(("1"
(expand "directed?")
(("1"
(inst - "x!1" "x!2")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(expand "+")
(("1"
(flatten)
(("1"
(assert)
(("1"
(flatten)
(("1"
(inst
+
"right(x!2)")
(("1"
(assert)
(("1"
(decompose-equality)
nil
nil))
nil)
("2"
(expand
"RD")
(("2"
(assert)
(("2"
(case-replace
"inr(right[T1, T2](x!2))=x!2")
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand "image")
(("2"
(skosimp)
(("2"
(replace -1)
(("2"
(typepred "x!3")
(("2"
(expand "RD")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((directed_complete? const-decl "bool" directed_orders nil)
(partial_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil sum_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(+ const-decl "bool" sum_orders nil)
(directed? const-decl "bool" directed_orders nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil) (union type-decl nil union_adt nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(inr adt-constructor-decl "[T2 -> (inr?)]" union_adt nil)
(x!2 skolem-const-decl "union[T1, T2]" sum_orders nil)
(RD skolem-const-decl "[T2 -> bool]" sum_orders nil)
(right adt-accessor-decl "[(inr?) -> T2]" union_adt nil)
(r!2 skolem-const-decl "(RD)" sum_orders nil)
(union_inr_extensionality formula-decl nil union_adt nil)
(z!1 skolem-const-decl "(D!1)" sum_orders nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(inl adt-constructor-decl "[T1 -> (inl?)]" union_adt nil)
(image const-decl "set[R]" function_image nil)
(x!1 skolem-const-decl "union[T1, T2]" sum_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(left adt-accessor-decl "[(inl?) -> T1]" union_adt nil)
(inr? adt-recognizer-decl "[union -> boolean]" union_adt nil)
(r!2 skolem-const-decl "(LD)" sum_orders nil)
(D!1 skolem-const-decl "(directed?(r1!1 + r2!1))" sum_orders nil)
(r2!1 skolem-const-decl "(directed_complete?[T2])" sum_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(r1!1 skolem-const-decl "(directed_complete?[T1])" sum_orders nil)
(LD skolem-const-decl "[T1 -> bool]" sum_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(sum_preserves_partial_order application-judgement
"(partial_order?[union[T1, T2]])" sum_orders nil)
(x!2 skolem-const-decl "union[T1, T2]" sum_orders nil)
(union_inl_extensionality formula-decl nil union_adt nil)
(inl? adt-recognizer-decl "[union -> boolean]" union_adt nil)
(T1 formal-type-decl nil sum_orders nil))
nil))
(sum_preserves_directed_complete_partial_order 0
(sum_preserves_directed_complete_partial_order-1 nil 3353304649
("" (skosimp)
(("" (typepred "r2!1")
(("" (typepred "r1!1")
(("" (expand "directed_complete_partial_order?")
(("" (flatten)
((""
(lemma "sum_preserves_directed_complete"
("r1" "r1!1" "r2" "r2!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)
("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(pred type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil sum_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sum_preserves_partial_order application-judgement
"(partial_order?[union[T1, T2]])" sum_orders nil)
(directed_complete? const-decl "bool" directed_orders nil)
(partial_order? const-decl "bool" orders nil)
(sum_preserves_directed_complete judgement-tcc nil sum_orders nil)
(T1 formal-type-decl nil sum_orders nil))
nil)))
¤ Dauer der Verarbeitung: 0.57 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.
|
