| products/Sources/formale Sprachen/PVS/TRS/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: inductive.mli Sprache: LispOriginal von: PVS© |
|
||||||
|
(IUnion_extra
(upto?_TCC1 0 (upto?_TCC1-1 nil 3415314220 ("" (subtype-tcc) nil nil) nil nil)) (disjoint_subset 0 (disjoint_subset-1 nil 3415314271 ("" (skosimp*) (("" (expand* "disjoint?" "empty?" "intersection") (("" (skeep) (("" (inst?) (("" (expand* "subset?" "member") (("" (inst?) (("" (inst?) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (T formal-type-decl nil IUnion_extra nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil)) shostak)) (disjoint_commute 0 (disjoint_commute-1 nil 3415314299 ("" (skeep) (("" (expand* "disjoint?" "empty?" "intersection") (("" (skosimp*) (("" (inst?) (("" (expand "member") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (T formal-type-decl nil IUnion_extra nil) (member const-decl "bool" sets nil)) shostak)) (IUnion_of_finite_is_finite 0 (IUnion_of_finite_is_finite-1 nil 3415314322 ("" (induct "n") (("1" (typepred "n!1") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (case "j!1 = 0") (("1" (hide -2) (("1" (expand "IUnion") (("1" (inst -3 "1") (("1" (case-replace "{x: T | EXISTS (i_1: upto?(1 + j!1)): f!1(i_1)(x)} = f!1(1)" :hide? T) (("1" (hide 2) (("1" (decompose-equality 1) (("1" (iff) (("1" (prop) (("1" (skosimp*) (("1" (typepred "i!1") (("1" (replaces -4) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst 1 "1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -1 "restrict[upto?(1 + j!1), upto?(j!1), set[T]](f!1)") (("2" (prop) (("1" (expand "restrict") (("1" (case-replace "IUnion(LAMBDA (i: upto?(1 + j!1)): f!1(i)) = union(f!1(j!1 + 1),IUnion(LAMBDA ( :hide? T) (("1" (inst -3 "j!1 + 1") (("1" (rewrite "finite_union" 2) nil nil)) nil) ("2" (hide (-1 -3 3)) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "IUnion" -1) (("1" (skosimp*) (("1" (expand* "union" "member") (("1" (flatten) (("1" (case-replace "i!1 = 1 + j!1") (("1" (expand "IUnion") (("1" (inst 3 "i!1") (("1" (typepred "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "union" "member") (("2" (prop) (("1" (expand "IUnion") (("1" (inst 1 "1 + j!1") nil nil)) nil) ("2" (expand "IUnion") (("2" (skosimp*) (("2" (inst 1 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "restrict") (("2" (inst -2 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((union const-decl "set" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (finite_set type-eq-decl nil finite_sets nil) (finite_union judgement-tcc nil finite_sets nil) (i!1 skolem-const-decl "upto?(1 + j!1)" IUnion_extra nil) (j!1 skolem-const-decl "nat" IUnion_extra nil) (member const-decl "bool" sets nil) (restrict const-decl "R" restrict nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (IUnion const-decl "set[T]" indexed_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil IUnion_extra nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (<= const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (IUnion_of_finite_is_finite1 0 (IUnion_of_finite_is_finite1-1 nil 3415319375 ("" (induct "n") (("1" (typepred "n!1") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (case "j!1 = 0") (("1" (hide -2) (("1" (expand "IUnion") (("1" (inst -3 "0") (("1" (case-replace "{x: T | EXISTS (i_1: below[1 + j!1]): f!1(i_1)(x)} = f!1(0)" :hide? T) (("1" (hide 2) (("1" (decompose-equality 1) (("1" (iff) (("1" (prop) (("1" (skosimp*) (("1" (typepred "i!1") (("1" (replaces -3) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst 1 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -1 "restrict[below[1 + j!1], below[j!1], set[T]](f!1)") (("2" (prop) (("1" (expand "restrict") (("1" (case-replace "IUnion(LAMBDA (i: below[1 + j!1]): f!1(i)) = union(f!1(j!1),IUnion(LAMBDA (i: b :hide? T) (("1" (inst -3 "j!1") (("1" (rewrite "finite_union" 2) nil nil)) nil) ("2" (hide (-1 -3 3)) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "IUnion" -1) (("1" (skosimp*) (("1" (expand* "union" "member") (("1" (flatten) (("1" (case-replace "i!1 = j!1") (("1" (expand "IUnion") (("1" (inst 3 "i!1") (("1" (typepred "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "union" "member") (("2" (prop) (("1" (expand "IUnion") (("1" (inst 1 "j!1") nil nil)) nil) ("2" (expand "IUnion") (("2" (skosimp*) (("2" (inst 1 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "restrict") (("2" (inst -2 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((union const-decl "set" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (finite_set type-eq-decl nil finite_sets nil) (finite_union judgement-tcc nil finite_sets nil) (i!1 skolem-const-decl "below[1 + j!1]" IUnion_extra nil) (j!1 skolem-const-decl "nat" IUnion_extra nil) (member const-decl "bool" sets nil) (restrict const-decl "R" restrict nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat_induction formula-decl nil naturalnumbers nil) (IUnion const-decl "set[T]" indexed_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil IUnion_extra nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak))) ¤ Dauer der Verarbeitung: 0.3 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 |
