|
(product_orders
(product_preserves_reflexive 0
(product_preserves_reflexive-1 nil 3353154167
("" (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 product_orders nil)
(PRED type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil product_orders nil)
(* const-decl "bool" product_orders nil)
(reflexive? const-decl "bool" relations nil))
nil))
(product_preserves_transitive 0
(product_preserves_transitive-1 nil 3353154167
("" (skosimp)
(("" (typepred "r1!1")
(("" (typepred "r2!1")
(("" (expand "*")
(("" (expand "transitive?")
(("" (skosimp)
(("" (inst - "x!1`2" "y!1`2" "z!1`2")
(("" (inst - "x!1`1" "y!1`1" "z!1`1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T1 formal-type-decl nil product_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" product_orders nil)
(T2 formal-type-decl nil product_orders nil))
nil))
(product_preserves_antisymmetric 0
(product_preserves_antisymmetric-1 nil 3353154167
("" (skosimp)
(("" (typepred "r1!1")
(("" (typepred "r2!1")
(("" (expand "*")
(("" (expand "antisymmetric?")
(("" (skosimp)
(("" (inst - "x!1`2" "y!1`2")
(("" (inst - "x!1`1" "y!1`1")
(("" (assert) (("" (decompose-equality) 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)
(T1 formal-type-decl nil product_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" product_orders nil)
(T2 formal-type-decl nil product_orders nil))
nil))
(product_preserves_preorder 0
(product_preserves_preorder-1 nil 3353154927
("" (judgement-tcc) nil nil)
((product_preserves_transitive application-judgement
"(transitive?[[T1, T2]])" product_orders nil)
(product_preserves_reflexive application-judgement
"(reflexive?[[T1, T2]])" product_orders nil)
(preorder? const-decl "bool" orders nil))
nil))
(product_preserves_partial_order 0
(product_preserves_partial_order-1 nil 3353154927
("" (judgement-tcc) nil nil)
((product_preserves_antisymmetric application-judgement
"(antisymmetric?[[T1, T2]])" product_orders nil)
(product_preserves_preorder application-judgement
"(preorder?[[T1, T2]])" product_orders nil)
(partial_order? const-decl "bool" orders nil))
nil))
(product_preserves_directed_complete 0
(product_preserves_directed_complete-1 nil 3353154927
("" (skosimp)
(("" (typepred "r2!1")
(("" (typepred "r1!1")
(("" (expand "*")
(("" (expand "directed_complete?")
(("" (skosimp)
(("" (typepred "D!1")
(("" (name "DD1" "{x:T1 | EXISTS (z:(D!1)): z`1 = x}")
((""
(name "DD2" "{y:T2 | EXISTS (z:(D!1)): z`2 = y}")
(("" (inst - "DD1")
(("1" (inst - "DD2")
(("1" (expand "least_bounded_above?")
(("1" (skosimp*)
(("1" (inst + "(t!1,t!2)")
(("1"
(expand "least_upper_bound?")
(("1"
(expand "upper_bound?")
(("1"
(flatten)
(("1"
(split 1)
(("1"
(skosimp)
(("1"
(inst -6 "r!1`1")
(("1"
(inst -9 "r!1`2")
(("1" (assert) nil nil)
("2"
(expand "DD2")
(("2"
(inst + "r!1")
nil
nil))
nil))
nil)
("2"
(expand "DD1")
(("2"
(inst + "r!1")
nil
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst -8 "r!1`1")
(("2"
(inst -11 "r!1`2")
(("2"
(split -8)
(("1"
(split -11)
(("1" (assert) nil nil)
("2"
(skosimp)
(("2"
(typepred "r!2")
(("2"
(expand "DD2")
(("2"
(skosimp)
(("2"
(inst
-3
"z!1")
(("2"
(flatten)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(typepred "r!2")
(("2"
(expand "DD1")
(("2"
(skosimp)
(("2"
(inst -2 "z!1")
(("2"
(flatten)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -2 -5 -6 2)
(("2" (case-replace "nonempty?[T2](DD2)")
(("1" (expand "directed?")
(("1"
(skosimp)
(("1"
(expand "DD2")
(("1"
(skosimp*)
(("1"
(inst - "z!1" "z!2")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst + "z!3`2")
(("1" (assert) nil nil)
("2"
(expand "DD2")
(("2"
(inst + "z!3")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(skosimp)
(("2"
(expand "member")
(("2"
(inst - "x!1`2")
(("2"
(expand "DD2")
(("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -2 -6 -7 2)
(("2" (case-replace "nonempty?[T1](DD1)")
(("1" (expand "directed?")
(("1" (skosimp)
(("1"
(expand "DD1")
(("1"
(skosimp*)
(("1"
(inst - "z!1" "z!2")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst + "z!3`1")
(("1" (assert) nil nil)
("2"
(expand "DD1")
(("2"
(inst + "z!3")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2 -3)
(("2" (expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(skosimp)
(("2"
(expand "member")
(("2"
(inst - "x!1`1")
(("2"
(expand "DD1")
(("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)
((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 product_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" product_orders nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(DD1 skolem-const-decl "[T1 -> boolean]" product_orders nil)
(r1!1 skolem-const-decl "(directed_complete?[T1])" product_orders
nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "[T1, T2]" product_orders nil)
(z!3 skolem-const-decl "(D!1)" product_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(D!1 skolem-const-decl
"(directed?(LAMBDA (x, y): r1!1(x`1, y`1) AND r2!1(x`2, y`2)))"
product_orders nil)
(r!1 skolem-const-decl "(D!1)" product_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(r2!1 skolem-const-decl "(directed_complete?[T2])" product_orders
nil)
(DD2 skolem-const-decl "[T2 -> boolean]" product_orders nil)
(z!3 skolem-const-decl "(D!1)" product_orders nil)
(x!1 skolem-const-decl "[T1, T2]" product_orders nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(directed? const-decl "bool" directed_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T1 formal-type-decl nil product_orders nil))
nil))
(product_preserves_directed_complete_partial_order 0
(product_preserves_directed_complete_partial_order-1 nil 3353154927
("" (skosimp)
(("" (typepred "r2!1")
(("" (typepred "r1!1")
(("" (expand "directed_complete_partial_order?")
(("" (flatten)
((""
(lemma "product_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 product_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(product_preserves_partial_order application-judgement
"(partial_order?[[T1, T2]])" product_orders nil)
(directed_complete? const-decl "bool" directed_orders nil)
(partial_order? const-decl "bool" orders nil)
(product_preserves_directed_complete judgement-tcc nil
product_orders nil)
(T1 formal-type-decl nil product_orders nil))
nil))
(product_lub_TCC1 0
(product_lub_TCC1-1 nil 3353466317
("" (skosimp)
((""
(lemma "product_preserves_directed_complete"
("r1" "r1!1" "r2" "r2!1"))
(("1" (expand "directed_complete?")
(("1" (inst - "D!1") nil nil)) nil)
("2" (typepred "r2!1")
(("2" (expand "directed_complete_partial_order?")
(("2" (flatten) nil nil)) nil))
nil)
("3" (typepred "r1!1")
(("3" (expand "directed_complete_partial_order?")
(("3" (flatten) nil nil)) nil))
nil))
nil))
nil)
((T2 formal-type-decl nil product_orders nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(directed_complete? const-decl "bool" directed_orders nil)
(partial_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil product_orders nil)
(product_preserves_directed_complete judgement-tcc nil
product_orders nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(directed? const-decl "bool" directed_orders nil)
(* const-decl "bool" product_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(product_lub_TCC2 0
(product_lub_TCC2-1 nil 3353466317
("" (skosimp)
(("" (typepred "D!1")
(("" (typepred "r1!1")
(("" (typepred "r2!1")
(("" (expand "directed_complete_partial_order?")
(("" (flatten)
((""
(lemma "product_preserves_directed_complete"
("r1" "r1!1" "r2" "r2!1"))
(("1" (hide -2 -3)
(("1" (expand "directed_complete?")
(("1" (inst - "D!1")
(("1"
(name-replace "D1"
"{x: T1 | EXISTS (z: (D!1)): z`1 = x}")
(("1" (case "nonempty?(D1)")
(("1" (case "directed?(r1!1)(D1)")
(("1" (inst - "D1") nil nil)
("2" (hide-all-but (1 -6))
(("2"
(expand "directed?")
(("2"
(skosimp)
(("2"
(expand "D1")
(("2"
(skosimp*)
(("2"
(inst - "z!1" "z!2")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(expand "*")
(("2"
(flatten)
(("2"
(inst + "z!3`1")
(("1"
(assert)
nil
nil)
("2"
(expand "D1")
(("2"
(inst + "z!3")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil))
nil)
("2" (hide-all-but (-4 1))
(("2" (expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(skosimp)
(("2"
(expand "member")
(("2"
(expand "D1")
(("2"
(inst - "x!1`1")
(("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(* const-decl "bool" product_orders nil)
(directed? const-decl "bool" directed_orders nil)
(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)
(T2 formal-type-decl nil product_orders nil)
(T1 formal-type-decl nil product_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(z!3 skolem-const-decl "(D!1)" product_orders nil)
(D!1 skolem-const-decl "(directed?[[T1, T2]](r1!1 * r2!1))"
product_orders nil)
(r2!1 skolem-const-decl "(directed_complete_partial_order?[T2])"
product_orders nil)
(r1!1 skolem-const-decl "(directed_complete_partial_order?[T1])"
product_orders nil)
(D1 skolem-const-decl "[T1 -> boolean]" product_orders nil)
(x!1 skolem-const-decl "[T1, T2]" product_orders nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(directed_complete? const-decl "bool" directed_orders nil)
(product_preserves_directed_complete judgement-tcc nil
product_orders nil))
nil))
(product_lub_TCC3 0
(product_lub_TCC3-1 nil 3353466317
("" (skosimp)
(("" (typepred "D!1")
(("" (name-replace "D2" "{y: T2 | EXISTS (z: (D!1)): z`2 = y}")
(("" (typepred "r2!1")
(("" (typepred "r1!1")
(("" (expand "directed_complete_partial_order?")
(("" (flatten)
(("" (hide -1 -3)
((""
(lemma "product_preserves_directed_complete"
("r1" "r1!1" "r2" "r2!1"))
(("1" (case "nonempty?(D2)")
(("1" (case "directed?(r2!1)(D2)")
(("1" (expand "directed_complete?")
(("1" (inst -5 "D2") nil nil)) nil)
("2" (hide-all-but (-6 1))
(("2" (expand "directed?")
(("2" (skosimp)
(("2"
(expand "D2")
(("2"
(skosimp*)
(("2"
(inst - "z!1" "z!2")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(expand "*")
(("2"
(flatten)
(("2"
(inst + "z!3`2")
(("1" (assert) nil nil)
("2"
(expand "D2")
(("2"
(inst + "z!3")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil))
nil)
("2" (hide-all-but (-4 1))
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (skosimp)
(("2"
(expand "member")
(("2"
(expand "D2")
(("2"
(inst - "x!1`2")
(("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(* const-decl "bool" product_orders nil)
(directed? const-decl "bool" directed_orders nil)
(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)
(T2 formal-type-decl nil product_orders nil)
(T1 formal-type-decl nil product_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(z!3 skolem-const-decl "(D!1)" product_orders nil)
(D!1 skolem-const-decl "(directed?[[T1, T2]](r1!1 * r2!1))"
product_orders nil)
(r1!1 skolem-const-decl "(directed_complete_partial_order?[T1])"
product_orders nil)
(D2 skolem-const-decl "[T2 -> boolean]" product_orders nil)
(r2!1 skolem-const-decl "(directed_complete_partial_order?[T2])"
product_orders nil)
(x!1 skolem-const-decl "[T1, T2]" product_orders nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(directed_complete? const-decl "bool" directed_orders nil)
(product_preserves_directed_complete judgement-tcc nil
product_orders nil)
(= const-decl "[T, T -> boolean]" equalities nil))
nil))
(product_lub 0
(product_lub-1 nil 3353505738
("" (skosimp)
(("" (typepred "D!1")
(("" (typepred "r1!1")
(("" (typepred "r2!1")
(("" (expand "directed_complete_partial_order?")
(("" (flatten)
((""
(lemma "product_preserves_directed_complete"
("r1" "r1!1" "r2" "r2!1"))
(("1" (expand "directed_complete?")
(("1" (inst - "D!1")
(("1" (typepred "lub(r1!1 * r2!1)(D!1)")
(("1"
(name-replace "LUB12" "lub(r1!1 * r2!1)(D!1)")
(("1"
(name-replace "D1"
"{x: T1 | EXISTS (z: (D!1)): z`1 = x}")
(("1"
(name-replace "D2"
"{y: T2 | EXISTS (z: (D!1)): z`2 = y}")
(("1" (case "nonempty?(D1)")
(("1"
(case "nonempty?(D2)")
(("1"
(case "directed?(r1!1)(D1)")
(("1"
(case "directed?(r2!1)(D2)")
(("1"
(inst - "D2")
(("1"
(inst - "D1")
(("1"
(typepred "lub(r1!1)(D1)")
(("1"
(typepred "lub(r2!1)(D2)")
(("1"
(name-replace
"LUB1"
"lub(r1!1)(D1)")
(("1"
(name-replace
"LUB2"
"lub(r2!1)(D2)")
(("1"
(hide-all-but
(-1 -2 -7 1 -9 -11))
(("1"
(expand
"least_upper_bound?")
(("1"
(flatten)
(("1"
(inst
-
"LUB12`2")
(("1"
(inst
-
"LUB12`1")
(("1"
(inst
-
"(LUB1,LUB2)")
(("1"
(lemma
"product_preserves_partial_order"
("r1"
"r1!1"
"r2"
"r2!1"))
(("1"
(expand
"upper_bound?")
(("1"
(expand
"*")
(("1"
(split
-3)
(("1"
(split
-5)
(("1"
(split
-7)
(("1"
(flatten)
(("1"
(expand
"partial_order?")
(("1"
(flatten)
(("1"
(expand
"antisymmetric?")
(("1"
(inst
-13
"LUB12`1"
"LUB1")
(("1"
(inst
-11
"LUB12`2"
"LUB2")
(("1"
(assert)
(("1"
(decompose-equality
1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(skosimp)
(("2"
(typepred
"r!1")
(("2"
(inst
-
"r!1`2")
(("1"
(inst
-
"r!1`1")
(("1"
(assert)
nil
nil)
("2"
(expand
"D1")
(("2"
(inst
+
"r!1")
nil
nil))
nil))
nil)
("2"
(expand
"D2")
(("2"
(inst
+
"r!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(skosimp)
(("2"
(typepred
"r!1")
(("2"
(expand
"D1")
(("2"
(skosimp)
(("2"
(inst
-6
"z!1")
(("2"
(flatten)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(skosimp)
(("2"
(typepred
"r!1")
(("2"
(expand
"D2")
(("2"
(skosimp)
(("2"
(inst
-6
"z!1")
(("2"
(flatten)
(("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)
("2"
(hide-all-but (-6 -11 1 -10 -2))
(("2"
(expand "*")
(("2"
(expand "D2")
(("2"
(expand "directed?")
(("2"
(skosimp*)
(("2"
(typepred "z!1")
(("2"
(typepred "z!2")
(("2"
(inst
-8
"z!1"
"z!2")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst
+
"z!3`2")
(("1"
(assert)
nil
nil)
("2"
(inst
+
"z!3")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil))
nil)
("2"
(hide-all-but (-10 1))
(("2"
(expand "D1")
(("2"
(expand "*")
(("2"
(expand "directed?")
(("2"
(skosimp*)
(("2"
(inst - "z!1" "z!2")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst + "z!3`1")
(("1"
(assert)
nil
nil)
("2"
(inst + "z!3")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil))
nil)
("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(hide-all-but (-1 2))
(("2"
(skosimp)
(("2"
(expand "member")
(("2"
(expand "D2")
(("2"
(inst - "x!1`2")
(("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(skosimp)
(("2"
(inst -1 "x!1`1")
(("2"
(expand "member")
(("2"
(expand "D1")
(("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(* const-decl "bool" product_orders nil)
(directed? const-decl "bool" directed_orders nil)
(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)
(T2 formal-type-decl nil product_orders nil)
(T1 formal-type-decl nil product_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(product_preserves_directed_complete_partial_order
application-judgement
"(directed_complete_partial_order?[[T1, T2]])" product_orders nil)
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "[T1, T2]" product_orders nil)
(empty? const-decl "bool" sets nil)
(z!3 skolem-const-decl "(D!1)" product_orders nil)
(r2!1 skolem-const-decl "(directed_complete_partial_order?[T2])"
product_orders nil)
(D2 skolem-const-decl "[T2 -> boolean]" product_orders nil)
(product_preserves_partial_order judgement-tcc nil product_orders
nil)
(r!1 skolem-const-decl "(D!1)" product_orders nil)
(D!1 skolem-const-decl "(directed?(r1!1 * r2!1))" product_orders
nil)
(antisymmetric? const-decl "bool" relations nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(D1 skolem-const-decl "[T1 -> boolean]" product_orders nil)
(r1!1 skolem-const-decl "(directed_complete_partial_order?[T1])"
product_orders nil)
(z!3 skolem-const-decl "(D!1)" product_orders nil)
(x!1 skolem-const-decl "[T1, T2]" product_orders nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(directed_complete? const-decl "bool" directed_orders nil)
(product_preserves_directed_complete judgement-tcc nil
product_orders nil))
shostak))
(product_preserves_has_least 0
(product_preserves_has_least-1 nil 3353155624
("" (skosimp)
(("" (expand "fullset")
(("" (expand "*")
(("" (expand "has_least?")
(("" (skosimp*)
(("" (expand "least?")
(("" (expand "lower_bound?")
(("" (inst + "(t!1,t!2)")
(("" (skosimp)
(("" (inst - "r!1`1")
(("" (inst - "r!1`2") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fullset const-decl "set" sets nil)
(has_least? const-decl "bool" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(T2 formal-type-decl nil product_orders nil)
(T1 formal-type-decl nil product_orders nil)
(TRUE const-decl "bool" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(* const-decl "bool" product_orders nil))
shostak))
(product_preserves_pointed_directed_complete_partial_order 0
(product_preserves_pointed_directed_complete_partial_order-1 nil
3353154927
("" (skosimp)
((""
(lemma "product_preserves_directed_complete_partial_order"
("r1" "r1!1" "r2" "r2!1"))
(("" (expand "pointed_directed_complete_partial_order?")
((""
(lemma "product_preserves_has_least"
("rel1" "r1!1" "rel2" "r2!1"))
(("" (typepred "r1!1")
(("" (typepred "r2!1")
(("" (expand "pointed_directed_complete_partial_order?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T2 formal-type-decl nil product_orders nil)
(pointed_directed_complete_partial_order? const-decl "bool"
directed_orders nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil product_orders nil)
(product_preserves_directed_complete_partial_order judgement-tcc
nil product_orders nil)
(product_preserves_has_least formula-decl nil product_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(product_preserves_directed_complete_partial_order
application-judgement
"(directed_complete_partial_order?[[T1, T2]])" product_orders
nil))
nil))
(product_least_TCC1 0
(product_least_TCC1-1 nil 3355018550
("" (skosimp)
((""
(lemma
"product_preserves_pointed_directed_complete_partial_order"
("r1" "r1!1" "r2" "r2!1"))
(("" (expand "pointed_directed_complete_partial_order?")
(("" (flatten) nil nil)) nil))
nil))
nil)
((T2 formal-type-decl nil product_orders nil)
(pointed_directed_complete_partial_order? const-decl "bool"
directed_orders nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil product_orders nil)
(product_preserves_pointed_directed_complete_partial_order
judgement-tcc nil product_orders nil)
(product_preserves_pointed_directed_complete_partial_order
application-judgement
"(pointed_directed_complete_partial_order?[[T1, T2]])"
product_orders nil))
nil))
(product_least_TCC2 0
(product_least_TCC2-1 nil 3355018550 ("" (subtype-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)
(pred type-eq-decl nil defined_types nil)
(pointed_directed_complete_partial_order? const-decl "bool"
directed_orders nil)
(T2 formal-type-decl nil product_orders nil)
(reflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(directed_complete? const-decl "bool" directed_orders nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(fullset const-decl "set" sets nil)
(T1 formal-type-decl nil product_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil))
nil))
(product_least_TCC3 0
(product_least_TCC3-1 nil 3355018550 ("" (subtype-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 product_orders nil)
(pred type-eq-decl nil defined_types nil)
(pointed_directed_complete_partial_order? const-decl "bool"
directed_orders nil)
(reflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(directed_complete? const-decl "bool" directed_orders nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(fullset const-decl "set" sets nil)
(T2 formal-type-decl nil product_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil))
nil))
(product_least 0
(product_least-1 nil 3355018561
("" (skosimp)
(("" (typepred "least(r1!1)(fullset[T1])")
(("" (typepred "least(r2!1)(fullset[T2])")
(("" (typepred "least(r1!1*r2!1)(fullset[[T1,T2]])")
((""
(name-replace "L12"
"least(r1!1 * r2!1)(fullset[[T1, T2]])")
(("" (name-replace "L1" "least(r1!1)(fullset[T1])")
(("" (name-replace "L2" "least(r2!1)(fullset[T2])")
(("" (expand "least?")
(("" (expand "fullset")
(("" (expand "lower_bound?")
(("" (inst -1 "(L1, L2)")
(("" (inst - "L12`2")
(("" (inst - "L12`1")
(("" (expand "*")
((""
(flatten)
((""
(typepred "r1!1")
((""
(typepred "r2!1")
((""
(expand
"pointed_directed_complete_partial_order?")
((""
(expand
"directed_complete_partial_order?")
((""
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.80Quellennavigators
Analyse erneut starten
]
|
