| products/Sources/formale Sprachen/PVS/examples/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: finite_enumeration.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.58 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.Bot Zugriff |
