|
(set_as_list_props
(strict_subset_card_lt 0
(strict_subset_card_lt-1 nil 3569753863
("" (skeep)
(("" (case "EXISTS (a : (s2)) : NOT s1(a)")
(("1" (skeep)
(("1" (typepred "a")
(("1" (case "subset?(add(a,s1),s2)")
(("1" (lemma "card_subset")
(("1" (inst? -1)
(("1" (assert)
(("1" (lemma "card_add")
(("1" (inst? -1) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "subset?")
(("2" (expand "strict_subset?")
(("2" (flatten)
(("2" (expand "subset?")
(("2" (expand "add")
(("2" (assert)
(("2" (skeep)
(("2" (expand "member" -1 1)
(("2" (assert)
(("2"
(inst? -3)
(("2"
(assert)
(("2"
(ground)
(("2"
(expand "member" 1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "strict_subset?")
(("2" (flatten)
(("2" (expand "subset?")
(("2" (apply-extensionality 2)
(("2" (inst 2 "x!1")
(("1" (expand "member" -2)
(("1" (inst? -2) (("1" (assert) nil nil)) nil)) nil)
("2" (assert)
(("2" (inst? -2)
(("2" (expand "member" -2) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil set_as_list_props nil)
(member const-decl "bool" sets nil)
(strict_subset? const-decl "bool" sets nil)
(card_subset formula-decl nil finite_sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(strict_subset_is_strict_order name-judgement
"(strict_order?[set[T]])" sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(card_add formula-decl nil finite_sets nil)
(nonempty_add_finite application-judgement
"non_empty_finite_set[T]" set_as_list_props nil)
(subset? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(x!1 skolem-const-decl "T" set_as_list_props nil)
(s2 skolem-const-decl "finite_set[T]" set_as_list_props nil))
shostak))
(empty_l2s 0
(empty_l2s-1 nil 3569743921 ("" (skeep) (("" (grind) nil nil)) nil)
((T formal-type-decl nil set_as_list_props nil)
(empty_sl? const-decl "bool" set_as_list nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(finite_emptyset name-judgement "finite_set" set_as_list_props nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(car adt-accessor-decl "[(cons?) -> T]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty_add_finite application-judgement
"non_empty_finite_set[T]" set_as_list_props nil))
shostak))
(emptyset_l2s 0
(emptyset_l2s-1 nil 3569743944 ("" (grind) nil nil)
((T formal-type-decl nil set_as_list_props nil)
(emptyset_sl const-decl "list[T]" set_as_list nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil)
(finite_emptyset name-judgement "finite_set" set_as_list_props nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
shostak))
(nonempty_l2s 0
(nonempty_l2s-1 nil 3569743952
("" (skeep) (("" (grind) nil nil)) nil)
((car adt-accessor-decl "[(cons?) -> T]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list_props nil)
(empty_sl? const-decl "bool" set_as_list nil)
(nonempty_sl? const-decl "bool" set_as_list nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil)
(member const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(nonempty_add_finite application-judgement
"non_empty_finite_set[T]" set_as_list_props nil)
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" set_as_list_props nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
shostak))
(subset_l2s 0
(subset_l2s-1 nil 3569743965
("" (skeep)
(("" (typepred "subset_sl?(l1, l2)")
(("" (typepred "list2set(l1)")
(("" (typepred "list2set(l2)")
(("" (rewrite -2)
(("" (rewrite -3)
(("" (hide -1 -2)
(("" (expand "subset?") (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset_sl? def-decl
"{b: bool | b IFF (FORALL x: member(x, l1) => member(x, l2))}"
set_as_list nil)
(member def-decl "bool" list_props nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil))
shostak))
(remove_l2s 0
(remove_l2s-1 nil 3569744079
("" (skeep)
(("" (typepred "remove_sl(x, l)")
(("" (typepred "list2set(remove_sl(x, l))")
(("" (typepred "list2set(l)")
(("" (hide -1 -3)
(("" (expand "remove")
(("" (rewrite -1)
(("" (rewrite -1)
(("" (apply-extensionality 1)
(("" (hide 2)
(("" (inst? -1)
(("" (rewrite -1)
(("" (expand "member" 1 2)
(("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((remove_sl def-decl
"{ll: list[T] | FORALL y: member(y, ll) IFF (x /= y AND member(y, l))}"
set_as_list nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(member def-decl "bool" list_props nil)
(list type-decl nil list_adt nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(remove const-decl "set" sets nil)
(member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil))
shostak))
(equal_l2s 0
(equal_l2s-1 nil 3569744229
("" (skeep)
(("" (typepred "list2set(l1)")
(("" (typepred "list2set(l2)")
(("" (typepred "equal_sl(l1, l2)")
(("" (hide -3 -5)
(("" (rewrite -3)
(("" (rewrite -3)
(("" (split 1)
(("1" (skosimp*)
(("1" (assert)
(("1" (hide -3)
(("1" (apply-extensionality 1)
(("1" (hide 2)
(("1" (inst? -2)
(("1" (rewrite -2) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (assert)
(("2" (hide -2)
(("2" (skeep)
(("2"
(case "FORALL x:({x: T | member[T](x, l1)})(x) = ({x: T | member[T](x, l2)})(x)")
(("1" (inst? -1)
(("1"
(rewrite -1)
(("1" (assert) nil nil))
nil))
nil)
("2" (rewrite -1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil)
(member def-decl "bool" list_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_set type-eq-decl nil finite_sets nil)
(list type-decl nil list_adt nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil set_as_list_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF member(x, l2))}"
set_as_list nil))
shostak))
(strict_subset_l2s 0
(strict_subset_l2s-1 nil 3569748385
("" (skeep)
(("" (lemma "equal_l2s")
(("" (lemma "subset_l2s")
(("" (expand "strict_subset?")
(("" (typepred "strict_subset_sl?(l1,l2)")
(("" (inst? -3)
(("" (inst? -4) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((equal_l2s formula-decl nil set_as_list_props nil)
(strict_subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(/= const-decl "boolean" notequal nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list_props nil)
(list type-decl nil list_adt nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(member def-decl "bool" list_props nil)
(subset_sl? def-decl
"{b: bool | b IFF (FORALL x: member(x, l1) => member(x, l2))}"
set_as_list nil)
(equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF member(x, l2))}"
set_as_list nil)
(strict_subset_sl? const-decl
"{b: bool | b IFF subset_sl?(l1, l2) & NOT equal_sl(l2, l1)}"
set_as_list nil)
(subset_l2s formula-decl nil set_as_list_props nil))
shostak))
(union_l2s 0
(union_l2s-1 nil 3569748758
("" (skeep)
(("" (typepred "list2set(union_sl(l1, l2))")
(("" (rewrite -2)
(("" (typepred "(union_sl(l1, l2))")
(("" (expand "union")
(("" (apply-extensionality 1)
(("" (hide 2)
(("" (inst? -1)
(("" (typepred "list2set(l1)")
(("" (typepred "list2set(l2)")
(("" (expand "member" 1 (2 3))
(("" (rewrite -2)
(("" (rewrite -3)
(("" (assert) (("" (rewrite -3) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((union_sl def-decl
"{ll: list[T] | FORALL x: member(x, ll) IFF (member(x, l1) OR member(x, l2))}"
set_as_list nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil)
(member def-decl "bool" list_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_set type-eq-decl nil finite_sets nil)
(list type-decl nil list_adt nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil set_as_list_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil))
shostak))
(intersection_l2s 0
(intersection_l2s-1 nil 3569749499
("" (skeep)
(("" (typepred "(intersection_sl(l1, l2))")
(("" (typepred "list2set(l1)")
(("" (typepred "list2set(l2)")
(("" (typepred "list2set(intersection_sl(l1, l2))")
(("" (rewrite -2)
(("" (expand "intersection")
(("" (apply-extensionality 1)
(("" (hide 2)
(("" (inst? -6)
(("" (rewrite -3)
(("" (rewrite -4)
(("" (expand "member" 1 (2 4))
(("" (rewrite -4) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((intersection_sl def-decl "{ll: list[T] |
FORALL x: member(x, ll) IFF (member(x, l1) AND member(x, l2))}"
set_as_list nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(member def-decl "bool" list_props nil)
(list type-decl nil list_adt nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil))
shostak))
(disjoint_l2s 0
(disjoint_l2s-1 nil 3569750548
("" (skeep)
(("" (expand "disjoint_sl?")
(("" (expand "disjoint?")
(("" (lemma "empty_l2s")
(("" (lemma "intersection_l2s")
(("" (inst? -2)
(("" (inst? -1) (("" (rewrite -1) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((disjoint_sl? const-decl "bool" set_as_list nil)
(empty_l2s formula-decl nil set_as_list_props nil)
(T formal-type-decl nil set_as_list_props nil)
(list type-decl nil list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(member def-decl "bool" list_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(intersection_sl def-decl "{ll: list[T] |
FORALL x: member(x, ll) IFF (member(x, l1) AND member(x, l2))}"
set_as_list nil)
(intersection_l2s formula-decl nil set_as_list_props nil)
(disjoint? const-decl "bool" sets nil)
(finite_intersection2 application-judgement "finite_set[T]"
set_as_list_props nil))
shostak))
(difference_l2s 0
(difference_l2s-1 nil 3569750786
("" (skeep)
(("" (typepred "difference_sl(l1, l2)")
(("" (typepred "list2set(difference_sl(l1, l2))")
(("" (rewrite -2)
(("" (apply-extensionality 1)
(("" (hide 2)
(("" (inst? -2)
(("" (expand "difference")
(("" (typepred "list2set(l2)")
(("" (typepred "list2set(l1)")
(("" (rewrite -2)
(("" (rewrite -3)
(("" (expand "member" 1 (2 4))
(("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((difference_sl def-decl "{ll: list[T] |
FORALL x: member(x, ll) IFF (member(x, l1) AND NOT member(x, l2))}"
set_as_list nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(member def-decl "bool" list_props nil)
(list type-decl nil list_adt nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(finite_difference application-judgement "finite_set[T]"
set_as_list_props nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil))
shostak))
(symmetric_difference_l2s 0
(symmetric_difference_l2s-1 nil 3569750932
("" (skeep)
(("" (expand "symmetric_difference")
(("" (expand "symmetric_difference_sl")
(("" (lemma "union_l2s")
(("" (lemma "difference_l2s")
(("" (inst-cp -1 "l1" "l2")
(("" (inst -1 "l2" "l1")
(("" (inst? -3)
(("" (rewrite -3)
(("" (rewrite -1) (("" (rewrite -1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((symmetric_difference const-decl "set" sets nil)
(union_l2s formula-decl nil set_as_list_props nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(member def-decl "bool" list_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(difference_sl def-decl "{ll: list[T] |
FORALL x: member(x, ll) IFF (member(x, l1) AND NOT member(x, l2))}"
set_as_list nil)
(finite_difference application-judgement "finite_set[T]"
set_as_list_props nil)
(finite_union application-judgement "finite_set[T]"
set_as_list_props nil)
(difference_l2s formula-decl nil set_as_list_props nil)
(symmetric_difference_sl const-decl "list[T]" set_as_list nil))
shostak))
(subset_sl_emptyset_sl 0
(subset_sl_emptyset_sl-1 nil 3569751060
("" (skeep) (("" (grind) nil nil)) nil)
((subset_sl? def-decl
"{b: bool | b IFF (FORALL x: member(x, l1) => member(x, l2))}"
set_as_list nil)
(emptyset_sl const-decl "list[T]" set_as_list nil)
(T formal-type-decl nil set_as_list_props nil))
shostak))
(subset_sl_reflexive 0
(subset_sl_reflexive-1 nil 3569751076
("" (skeep)
(("" (typepred "subset_sl?(l,l)")
(("" (assert) (("" (skeep) nil nil)) nil)) nil))
nil)
((subset_sl? def-decl
"{b: bool | b IFF (FORALL x: member(x, l1) => member(x, l2))}"
set_as_list nil)
(member def-decl "bool" list_props nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(subset_sl_transitive 0
(subset_sl_transitive-1 nil 3569751135
("" (skeep)
(("" (typepred "subset_sl?(l1,l)")
(("" (typepred "subset_sl?(l,l2)")
(("" (typepred "subset_sl?(l1,l2)")
(("" (assert)
(("" (hide -1 -3 -5 -6 -7 2) (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((subset_sl? def-decl
"{b: bool | b IFF (FORALL x: member(x, l1) => member(x, l2))}"
set_as_list nil)
(member def-decl "bool" list_props nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(subset_sl_preorder 0
(subset_sl_preorder-1 nil 3569751307
("" (expand "preorder?")
(("" (expand "reflexive?")
(("" (expand "transitive?")
(("" (lemma "subset_sl_reflexive")
(("" (lemma "subset_sl_transitive")
(("" (split 1)
(("1" (propax) nil nil)
("2" (skeep)
(("2" (inst -3 "y" "x" "z") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((reflexive? const-decl "bool" relations nil)
(subset_sl_reflexive formula-decl nil set_as_list_props nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list_props nil)
(subset_sl_transitive formula-decl nil set_as_list_props nil)
(transitive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil))
shostak))
(subset_sl_is_preorder 0
(subset_sl_is_preorder-1 nil 3569754755
("" (lemma "subset_sl_preorder") (("" (propax) nil nil)) nil)
((subset_sl_preorder formula-decl nil set_as_list_props nil)) nil))
(equal_sl_reflexive 0
(equal_sl_reflexive-1 nil 3569751739
("" (skeep)
(("" (expand "equal_sl")
(("" (lemma "subset_sl_reflexive")
(("" (inst? -1) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF member(x, l2))}"
set_as_list nil)
(T formal-type-decl nil set_as_list_props nil)
(list type-decl nil list_adt nil)
(subset_sl_is_preorder name-judgement "(preorder?[list[T]])"
set_as_list_props nil)
(subset_sl_reflexive formula-decl nil set_as_list_props nil))
shostak))
(equal_sl_transitive 0
(equal_sl_transitive-1 nil 3569751781
("" (skeep)
(("" (lemma "subset_sl_transitive")
(("" (expand "equal_sl")
(("" (flatten)
(("" (inst-cp -1 "l" "l2" "l1")
(("" (inst-cp -1 "l" "l1" "l2") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset_sl_transitive formula-decl nil set_as_list_props nil)
(subset_sl_is_preorder name-judgement "(preorder?[list[T]])"
set_as_list_props nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list_props nil)
(equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF member(x, l2))}"
set_as_list nil))
shostak))
(equal_sl_symmetric 0
(equal_sl_symmetric-1 nil 3569751886
("" (skeep)
(("" (expand "equal_sl") (("" (assert) (("" (grind) nil nil)) nil))
nil))
nil)
((equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF member(x, l2))}"
set_as_list nil)
(subset_sl_is_preorder name-judgement "(preorder?[list[T]])"
set_as_list_props nil))
shostak))
(strict_subset_sl_irreflexive 0
(strict_subset_sl_irreflexive-1 nil 3569751433
("" (skosimp*)
(("" (expand "strict_subset_sl?")
(("" (lemma "subset_sl_reflexive")
(("" (inst? -1) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((strict_subset_sl? const-decl
"{b: bool | b IFF subset_sl?(l1, l2) & NOT equal_sl(l2, l1)}"
set_as_list nil)
(T formal-type-decl nil set_as_list_props nil)
(list type-decl nil list_adt nil)
(subset_sl_is_preorder name-judgement "(preorder?[list[T]])"
set_as_list_props nil)
(subset_sl_reflexive formula-decl nil set_as_list_props nil))
shostak))
(strict_subset_sl_transitive 0
(strict_subset_sl_transitive-1 nil 3569751509
("" (skeep)
(("" (typepred "strict_subset_sl?(l1,l2)")
(("" (assert)
(("" (hide 2)
(("" (hide -1)
(("" (typepred "strict_subset_sl?(l1,l)")
(("" (typepred "strict_subset_sl?(l,l2)")
(("" (assert)
(("" (hide -2 -4)
(("" (flatten)
(("" (hide -3 -4)
(("" (lemma "subset_sl_transitive")
(("" (inst -1 "l" "l1" "l2")
(("" (assert)
((""
(expand "equal_sl")
((""
(lemma "subset_sl_transitive")
((""
(inst -1 "l1" "l2" "l")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((strict_subset_sl? const-decl
"{b: bool | b IFF subset_sl?(l1, l2) & NOT equal_sl(l2, l1)}"
set_as_list nil)
(equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF member(x, l2))}"
set_as_list nil)
(subset_sl? def-decl
"{b: bool | b IFF (FORALL x: member(x, l1) => member(x, l2))}"
set_as_list nil)
(member def-decl "bool" list_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset_sl_transitive formula-decl nil set_as_list_props nil)
(subset_sl_is_preorder name-judgement "(preorder?[list[T]])"
set_as_list_props nil))
shostak))
(strict_subset_sl_strict_order 0
(strict_subset_sl_strict_order-1 nil 3569752144
("" (expand "strict_order?")
(("" (expand "irreflexive?")
(("" (lemma "strict_subset_sl_irreflexive")
(("" (lemma "strict_subset_sl_transitive")
(("" (expand "transitive?")
(("" (split)
(("1" (propax) nil nil)
("2" (skeep)
(("2" (inst -3 "y" "x" "z") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((irreflexive? const-decl "bool" relations nil)
(strict_subset_sl_transitive formula-decl nil set_as_list_props
nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list_props nil)
(transitive? const-decl "bool" relations nil)
(strict_subset_sl_irreflexive formula-decl nil set_as_list_props
nil)
(strict_order? const-decl "bool" orders nil))
shostak))
(strict_subset_sl_is_strict_order 0
(strict_subset_sl_is_strict_order-1 nil 3569743910
("" (lemma "strict_subset_sl_strict_order") (("" (propax) nil nil))
nil)
((strict_subset_sl_strict_order formula-decl nil set_as_list_props
nil))
nil))
(strict_subset_sl_wf 0
(strict_subset_sl_wf-1 nil 3569752372
("" (expand "well_founded?")
(("" (skeep)
(("" (skeep)
(("" (lemma "wf_nat")
(("" (expand "well_founded?")
((""
(inst -1
"LAMBDA (n:nat) : EXISTS (l: list[T]): length(reduce_sl(l)) = n AND p(l)")
(("" (split -1)
(("1" (skeep)
(("1" (typepred "y!1")
(("1" (skeep)
(("1" (inst 1 "l")
(("1" (skeep)
(("1" (inst -3 "length(reduce_sl(x))")
(("1" (rewrite -1 :dir RL)
(("1"
(typepred "reduce_sl(x)")
(("1"
(typepred "reduce_sl(l)")
(("1"
(lemma "equal_l2s")
(("1"
(typepred
"card_sl(reduce_sl(x))")
(("1"
(typepred
"card_sl(reduce_sl(l))")
(("1"
(rewrite -5 :dir RL)
(("1"
(rewrite -6 :dir RL)
(("1"
(inst-cp
-3
"l"
"reduce_sl(l)")
(("1"
(inst
-3
"x"
"reduce_sl(x)")
(("1"
(rewrite -1)
(("1"
(rewrite -1)
(("1"
(rewrite -1)
(("1"
(rewrite -1)
(("1"
(hide -1)
(("1"
(rewrite
-1)
(("1"
(hide -1)
(("1"
(lemma
"strict_subset_l2s")
(("1"
(inst?
-1)
(("1"
(rewrite
-1)
(("1"
(hide
-1)
(("1"
(rewrite
-1
:dir
RL)
(("1"
(rewrite
-1
:dir
RL)
(("1"
(lemma
"strict_subset_card_lt")
(("1"
(inst?
-1)
(("1"
(assert)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst 1 "x") (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (inst 1 "length(reduce_sl(y))")
(("2" (inst 1 "y") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((wf_nat formula-decl nil naturalnumbers 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil set_as_list_props nil)
(list type-decl nil list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(length def-decl "nat" list_props nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(member def-decl "bool" list_props nil)
(equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF member(x, l2))}"
set_as_list nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil)
(card_sl def-decl "{n: nat | n = Card(list2set(l))}" set_as_list
nil)
(reduce_sl def-decl
"{ll: list[T] | equal_sl[T](l, ll) & card_sl(ll) = length(ll)}"
set_as_list nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(strict_subset_card_lt formula-decl nil set_as_list_props nil)
(strict_subset_is_strict_order name-judgement
"(strict_order?[set[T]])" sets_lemmas nil)
(strict_subset_l2s formula-decl nil set_as_list_props nil)
(equal_l2s formula-decl nil set_as_list_props nil)
(x skolem-const-decl "(p)" set_as_list_props nil)
(l skolem-const-decl "list[T]" set_as_list_props nil)
(p skolem-const-decl "pred[list[T]]" set_as_list_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(well_founded? const-decl "bool" orders nil))
shostak))
(strict_subset_sl_is_wf 0
(strict_subset_sl_is_wf-1 nil 3569754899
("" (lemma "strict_subset_sl_wf") (("" (propax) nil nil)) nil)
((strict_subset_sl_wf formula-decl nil set_as_list_props nil)) nil)))
¤ Dauer der Verarbeitung: 0.21 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.
|
