|
(set_as_list
(empty_sl_is_empty 0
(empty_sl_is_empty-1 nil 3591613697
("" (skosimp*)
(("" (split)
(("1" (skosimp*)
(("1" (expand "empty_sl?")
(("1" (rewrite -1)
(("1" (expand "member") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (generalize "l!1" l)
(("2" (induct l)
(("1" (expand "empty_sl?") (("1" (propax) nil nil)) nil)
("2" (skosimp*)
(("2" (inst -2 "cons1_var!1")
(("2" (expand "member" 1) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty_sl? const-decl "bool" set_as_list nil)
(member def-decl "bool" list_props nil)
(list_induction formula-decl nil list_adt nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list nil))
shostak))
(subset_sl?_TCC1 0
(subset_sl?_TCC1-1 nil 3569678532
("" (skeep)
(("" (rewrite -1)
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil)
((member def-decl "bool" list_props nil)) nil))
(subset_sl?_TCC2 0
(subset_sl?_TCC2-1 nil 3569678532 ("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
nil))
(subset_sl?_TCC3 0
(subset_sl?_TCC3-1 nil 3569678532
("" (skeep)
(("" (typepred "v(q, l2)")
(("1" (split 1)
(("1" (skosimp*)
(("1" (assert)
(("1" (rewrite -6)
(("1" (expand "member" -3)
(("1" (inst -4 "x!1") (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (assert)
(("2" (inst-cp -1 "a")
(("2" (rewrite -5)
(("2" (expand "member" -2 1)
(("2" (assert)
(("2" (skosimp*)
(("2" (expand "member" -1 1)
(("2" (inst -1 "x!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite -1)
(("2" (expand <<) (("2" (propax) nil nil)) nil)) nil))
nil))
nil)
((member def-decl "bool" list_props nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(strict_well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list 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))
nil))
(add_sl_TCC1 0
(add_sl_TCC1-1 nil 3569678532
("" (skosimp*)
(("" (expand "nonempty_sl?")
(("" (expand "empty_sl?")
(("" (rewrite -1)
(("" (expand "member" 1 2)
(("" (expand "member" 1)
(("" (expand "member" 1)
(("" (assert)
(("" (skosimp*)
(("" (split 1)
(("1" (ground) nil nil) ("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty_sl? const-decl "bool" set_as_list nil)
(member def-decl "bool" list_props nil)
(empty_sl? const-decl "bool" set_as_list nil))
nil))
(add_sl_TCC2 0
(add_sl_TCC2-1 nil 3569678532
("" (skeep)
(("" (rewrite -2)
(("" (split 1)
(("1" (grind) nil nil)
("2" (skosimp*)
(("2" (expand "member" 1) (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil)
((member def-decl "bool" list_props nil)
(nonempty_sl? const-decl "bool" set_as_list nil)
(empty_sl? const-decl "bool" set_as_list nil))
nil))
(add_sl_TCC3 0
(add_sl_TCC3-1 nil 3569678532
("" (skeep)
(("" (rewrite -1) (("" (expand <<) (("" (propax) nil nil)) nil))
nil))
nil)
((<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
nil))
(add_sl_TCC4 0
(add_sl_TCC4-1 nil 3569679497
("" (skeep)
(("" (ground)
(("1" (grind) nil nil)
("2" (typepred "v(x, q)")
(("1" (skeep)
(("1" (expand "member" 1 1)
(("1" (inst -2 "y")
(("1" (rewrite -2)
(("1" (rewrite -3)
(("1" (hide -2)
(("1" (expand "member" 1 2) (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite -1)
(("2" (expand <<) (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((empty_sl? const-decl "bool" set_as_list nil)
(nonempty_sl? const-decl "bool" set_as_list nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list nil)
(list type-decl nil list_adt nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(member def-decl "bool" list_props nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil))
nil))
(remove_sl_TCC1 0
(remove_sl_TCC1-1 nil 3569678532
("" (skeep)
(("" (rewrite -1)
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil)
((member def-decl "bool" list_props nil)) nil))
(remove_sl_TCC2 0
(remove_sl_TCC2-1 nil 3569678532 ("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
nil))
(remove_sl_TCC3 0
(remove_sl_TCC3-1 nil 3569678532
("" (skeep)
(("" (skeep)
(("" (typepred "v(x, q)")
(("" (inst -1 "y")
(("" (rewrite -3)
(("" (expand "member" 1 2)
(("" (rewrite -1)
(("" (hide -1) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(member def-decl "bool" list_props nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil))
nil))
(remove_sl_TCC4 0
(remove_sl_TCC4-1 nil 3569678532
("" (skeep)
(("" (skeep)
(("" (typepred "v(x, q)")
(("" (inst -1 "y")
(("" (rewrite -2)
(("" (expand "member" 2)
(("" (rewrite -1)
(("" (hide -1) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(member def-decl "bool" list_props nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil))
nil))
(equal_sl_TCC1 0
(equal_sl_TCC1-1 nil 3569678532
("" (skeep)
(("" (typepred "subset_sl?(l1, l2)")
(("" (typepred "subset_sl?(l2, l1)") (("" (grind) 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 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))
nil))
(strict_subset_sl?_TCC1 0
(strict_subset_sl?_TCC1-1 nil 3569678532
("" (skeep) (("" (expand "equal_sl") (("" (grind) 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))
nil))
(union_sl_TCC1 0
(union_sl_TCC1-1 nil 3569678532
("" (skeep)
(("" (rewrite -1)
(("" (expand "member" 1 2) (("" (propax) nil nil)) nil)) nil))
nil)
((member def-decl "bool" list_props nil)) nil))
(union_sl_TCC2 0
(union_sl_TCC2-1 nil 3569678532 ("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
nil))
(union_sl_TCC3 0
(union_sl_TCC3-1 nil 3569678532
("" (skeep)
(("" (skeep)
(("" (typepred "v(q, l2)")
(("" (typepred "add_sl(a, v(q, l2))")
(("" (rewrite -4)
(("" (inst -2 "x")
(("" (inst -3 "x")
(("" (rewrite -2)
(("" (rewrite -3)
(("" (expand "member" 1 3)
(("" (assert)
(("" (hide -1 -2 -3) (("" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((add_sl def-decl
"{ll: (nonempty_sl?) | FORALL y: member(y, ll) IFF (x = y OR member(y, l))}"
set_as_list nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonempty_sl? const-decl "bool" set_as_list nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(member def-decl "bool" list_props nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(OR const-decl "[bool, bool -> bool]" booleans nil))
nil))
(intersection_sl_TCC1 0
(intersection_sl_TCC1-1 nil 3569678532
("" (skosimp*)
(("" (rewrite -1)
(("" (expand "member" 1 (1 2)) (("" (propax) nil nil)) nil))
nil))
nil)
((member def-decl "bool" list_props nil)) nil))
(intersection_sl_TCC2 0
(intersection_sl_TCC2-1 nil 3569678532
("" (skeep)
(("" (skeep)
(("" (typepred "v(q, l2)")
(("" (expand "member" 1 1)
(("" (inst -1 "x")
(("" (rewrite -1)
(("" (hide -1)
(("" (rewrite -2)
(("" (expand "member" 1 3) (("" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(member def-decl "bool" list_props nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(intersection_sl_TCC3 0
(intersection_sl_TCC3-1 nil 3569678532
("" (skeep)
(("" (skeep)
(("" (typepred "v(q, l2)")
(("" (rewrite -2)
(("" (inst -1 "x")
(("" (rewrite -1)
(("" (hide -1)
(("" (expand "member" 2 3) (("" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(member def-decl "bool" list_props nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(difference_sl_TCC1 0
(difference_sl_TCC1-1 nil 3569678532
("" (skeep)
(("" (skeep)
(("" (rewrite -1)
(("" (expand "member" 1) (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((member def-decl "bool" list_props nil)) nil))
(difference_sl_TCC2 0
(difference_sl_TCC2-1 nil 3569678532
("" (skeep)
(("" (skeep)
(("" (typepred "v(q, l2)")
(("" (rewrite -3)
(("" (inst -1 "x")
(("" (rewrite -1)
(("" (hide -1)
(("" (expand "member" 1 3) (("" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(member def-decl "bool" list_props nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(difference_sl_TCC3 0
(difference_sl_TCC3-1 nil 3569678532
("" (skeep)
(("" (skeep)
(("" (typepred "v(q, l2)")
(("" (inst -1 "x")
(("" (rewrite -2)
(("" (expand "member" 2 (1 2))
(("" (rewrite -1)
(("" (hide -1) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil set_as_list nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(list type-decl nil list_adt nil)
(member def-decl "bool" list_props nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(list2set_TCC1 0
(list2set_TCC1-1 nil 3569678532
("" (skeep)
(("" (rewrite -1)
(("" (expand "member" 1)
(("" (ground)
(("" (expand "emptyset") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set" set_as_list nil)
(emptyset const-decl "set" sets nil)
(member def-decl "bool" list_props nil))
nil))
(list2set_TCC2 0
(list2set_TCC2-1 nil 3569678532
("" (skeep)
(("" (expand "add")
(("" (typepred "v(q)")
(("1" (rewrite -3)
(("1" (expand "member" 1 2)
(("1" (rewrite -2)
(("1" (expand "member" 1 1)
(("1" (assert)
(("1" (lemma "extensionality[T]")
(("1" (inst? -1)
(("1" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (skeep)
(("2" (expand "member" 1 (1 3))
(("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite -1)
(("2" (expand <<) (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((add const-decl "(nonempty?)" sets nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(extensionality formula-decl nil sets_lemmas 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)
(T formal-type-decl nil set_as_list nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(list type-decl nil list_adt nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(finite_set type-eq-decl nil finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(member def-decl "bool" list_props nil))
nil))
(card_sl_TCC1 0
(card_sl_TCC1-1 nil 3569678532
("" (skeep)
(("" (rewrite -1)
(("" (expand "list2set")
(("" (lemma "card_emptyset") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((T formal-type-decl nil set_as_list nil)
(card_emptyset formula-decl nil finite_sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set" set_as_list nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil))
nil))
(card_sl_TCC2 0
(card_sl_TCC2-1 nil 3569678532
("" (skeep)
(("" (typepred "v(q)")
(("" (typepred "list2set(l)")
(("" (typepred "list2set(q)")
(("" (rewrite -5)
(("" (case "list2set(q) = list2set(l)")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (rewrite -2)
(("2" (rewrite -3)
(("2" (apply-extensionality 1)
(("2" (hide 2)
(("2" (rewrite -4)
(("2" (expand "member" 1 2)
(("2" (case "x!1 = a")
(("1" (assert) nil nil)
("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)
(Card const-decl "nat" finite_sets 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(strict_well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(T formal-type-decl nil set_as_list nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(card_sl_TCC3 0
(card_sl_TCC3-1 nil 3569678532
("" (skeep)
(("" (typepred "list2set(q)")
(("" (lemma "card_add")
(("" (inst -1 "{x | member(x, q)}" "a")
(("1" (typepred "list2set(l)")
(("1" (rewrite -2)
(("1" (rewrite -5)
(("1" (expand "member" 2)
(("1" (hide -1)
(("1" (expand "add" -1)
(("1" (expand "member" -1 1)
(("1"
(case "{y: T | a = y OR member(y, q)} = {x | x = a OR member(x, q)}")
(("1" (rewrite -1) (("1" (assert) nil nil))
nil)
("2" (apply-extensionality 1)
(("2" (case "x!1 = a")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) 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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(q skolem-const-decl "list[T]" set_as_list nil)
(add const-decl "(nonempty?)" sets nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(member const-decl "bool" sets nil)
(card_add formula-decl nil finite_sets nil))
nil))
(reduce_sl_TCC1 0
(reduce_sl_TCC1-1 nil 3569739643
("" (expand "equal_sl")
(("" (skosimp*)
(("" (rewrite -1)
(("" (expand "subset_sl?") (("" (grind) 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)
(card_sl def-decl "{n: nat | n = Card(list2set(l))}" set_as_list
nil)
(length def-decl "nat" list_props nil)
(equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF member(x, l2))}"
set_as_list nil))
nil))
(reduce_sl_TCC2 0
(reduce_sl_TCC2-1 nil 3569739643
("" (skosimp*)
(("" (typepred "v!1(q!1)")
(("1" (split)
(("1" (expand "equal_sl" 1)
(("1" (expand "equal_sl" -1)
(("1" (flatten)
(("1" (split)
(("1" (expand "subset_sl?" 1)
(("1" (rewrite -5)
(("1" (assert)
(("1" (typepred "subset_sl?(q!1,v!1(q!1))")
(("1" (assert)
(("1" (inst? -1) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite -5)
(("2"
(typepred "subset_sl?(v!1(q!1), cons(a!1, q!1))")
(("2" (split -2)
(("1" (propax) nil nil)
("2" (typepred "subset_sl?(v!1(q!1), q!1)")
(("2" (skosimp*)
(("2" (expand "member" 1)
(("2" (assert)
(("2"
(flatten)
(("2"
(inst? -1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (rewrite -2) (("2" (grind) nil nil)) nil))
nil))
nil)
((length def-decl "nat" list_props nil)
(card_sl def-decl "{n: nat | n = Card(list2set(l))}" set_as_list
nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil)
(Card const-decl "nat" finite_sets 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(strict_well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF 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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
(subset_sl? def-decl
"{b: bool | b IFF (FORALL x: member(x, l1) => member(x, l2))}"
set_as_list nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil))
nil))
(reduce_sl_TCC3 0
(reduce_sl_TCC3-1 nil 3569739643
("" (skosimp*)
(("" (typepred "v!1(q!1)")
(("1" (rewrite -3)
(("1" (split)
(("1" (typepred "equal_sl[T](q!1, v!1(q!1))")
(("1"
(typepred
"equal_sl[T](cons(a!1, q!1), cons[T](a!1, v!1(q!1)))")
(("1" (assert)
(("1" (skosimp*)
(("1" (hide -1)
(("1" (hide -2)
(("1" (expand "member" 1)
(("1" (inst? -1) (("1" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "card_sl" 1)
(("2" (assert)
(("2" (typepred "equal_sl[T](q!1, v!1(q!1))")
(("2" (assert)
(("2" (hide -2)
(("2" (inst? -1)
(("2" (assert)
(("2" (expand "length" 2)
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite -1) (("2" (grind) nil nil)) nil))
nil))
nil)
((length def-decl "nat" list_props nil)
(card_sl def-decl "{n: nat | n = Card(list2set(l))}" set_as_list
nil)
(list2set def-decl "{s: finite_set[T] | s = ({x | member(x, l)})}"
set_as_list nil)
(Card const-decl "nat" finite_sets 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(strict_well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(equal_sl const-decl
"{b: bool | b IFF (FORALL x: member(x, l1) IFF 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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(equal_sl_card 0
(equal_sl_card-1 nil 3569741498
("" (skeep)
(("" (typepred "equal_sl(l1,l2)")
(("" (assert)
(("" (hide -2 -3)
(("" (typepred "card_sl(l1)")
(("" (typepred "card_sl(l2)")
(("" (typepred "list2set(l1)")
(("" (typepred "list2set(l2)")
(("" (hide -1 -3)
(("" (rewrite -1)
(("" (rewrite -1)
(("" (rewrite -1)
(("" (rewrite -1)
((""
(case "{x | member(x, l1)} = {x | member(x, l2)}")
(("1" (assert) nil nil)
("2"
(hide 2)
(("2"
(apply-extensionality 1)
(("2"
(inst? -1)
(("2" (rewrite -1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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 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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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))
shostak)))
¤ Dauer der Verarbeitung: 0.45 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.
|
