Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ordered_int.pvs Sprache: Lisp

Original von: PVS^©

(isomorphism
(isomorphism_implication 0
  (isomorphism_implication-1 nil 3315065653
   ("" (grind :if-match nil)
    (("1" (inst -6 "d1!1" "d2!1") (("1" (assert) nil nil)) nil)
     ("2" (inst -3 "d1!1" "d2!1")
      (("2" (inst -4 "f!1(d1!1)")
        (("2" (inst -4 "f!1(d1!1)" "f!1(d2!1)")
          (("2" (inst -5 "d2!1" "d1!1") (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil isomorphism nil)
    (R formal-type-decl nil isomorphism nil)
    (bijective? const-decl "bool" functions nil)
    (isomorphism? const-decl "bool" isomorphism nil)
    (preserves const-decl "bool" functions nil)
    (antisymmetric? const-decl "bool" relations nil)
    (irreflexive? const-decl "bool" relations nil)
    (trichotomous? const-decl "bool" orders nil))
   shostak))
(isomorphism_preserves_reflexive 0
  (isomorphism_preserves_reflexive-1 nil 3315065896
   ("" (grind) nil nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions nil)
    (R formal-type-decl nil isomorphism nil)
    (D formal-type-decl nil isomorphism nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (isomorphism? const-decl "bool" isomorphism nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (reflexive? const-decl "bool" relations nil))
   shostak))
(isomorphism_preserves_irreflexive 0
  (isomorphism_preserves_irreflexive-1 nil 3315065901
   ("" (grind) nil nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions nil)
    (R formal-type-decl nil isomorphism nil)
    (D formal-type-decl nil isomorphism nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (isomorphism? const-decl "bool" isomorphism nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (irreflexive? const-decl "bool" relations nil))
   shostak))
(isomorphism_preserves_symmetric 0
  (isomorphism_preserves_symmetric-1 nil 3315065906
   ("" (grind :if-match nil)
    (("1" (inst-cp - "y!1")
      (("1" (inst - "x!1")
        (("1" (skosimp*)
          (("1" (inst -5 "x!2" "x!3")
            (("1" (inst-cp -4 "x!3" "x!2")
              (("1" (inst -4 "x!2" "x!3") (("1" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (inst-cp -3 "y!1" "x!1")
      (("2" (inst -3 "x!1" "y!1")
        (("2" (inst -6 "f!1(x!1)" "f!1(y!1)") (("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil isomorphism nil)
    (R formal-type-decl nil isomorphism nil)
    (bijective? const-decl "bool" functions nil)
    (symmetric? const-decl "bool" relations nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak))
(isomorphism_preserves_antisymmetric 0
  (isomorphism_preserves_antisymmetric-1 nil 3315066236
   ("" (grind :if-match nil)
    (("1" (hide -1)
      (("1" (inst-cp - "y!1")
        (("1" (inst - "x!1")
          (("1" (skosimp*)
            (("1" (inst-cp - "x!3" "x!2")
              (("1" (inst - "x!2" "x!3")
                (("1" (inst - "x!2" "x!3") (("1" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (inst - "x!1" "y!1")
      (("2" (inst-cp - "y!1" "x!1")
        (("2" (inst - "x!1" "y!1")
          (("2" (inst - "f!1(x!1)" "f!1(y!1)") (("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil isomorphism nil)
    (R formal-type-decl nil isomorphism nil)
    (bijective? const-decl "bool" functions nil)
    (antisymmetric? const-decl "bool" relations nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak))
(isomorphism_preserves_asymmetric 0
  (isomorphism_preserves_asymmetric-1 nil 3318253850
   ("" (grind :if-match nil)
    (("1" (inst-cp - "y!1")
      (("1" (inst - "x!1")
        (("1" (skosimp*)
          (("1" (hide -1)
            (("1" (inst-cp - "x!3" "x!2")
              (("1" (inst - "x!2" "x!3")
                (("1" (inst - "x!2" "x!3") (("1" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (inst - "x!1" "y!1")
      (("2" (inst-cp - "y!1" "x!1")
        (("2" (inst - "x!1" "y!1")
          (("2" (inst - "f!1(x!1)" "f!1(y!1)") (("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bijective? const-decl "bool" functions nil)
    (R formal-type-decl nil isomorphism nil)
    (asymmetric? const-decl "bool" relations_extra nil)
    (D formal-type-decl nil isomorphism nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak))
(isomorphism_preserves_transitive 0
  (isomorphism_preserves_transitive-1 nil 3315066655
   ("" (grind :if-match nil)
    (("1" (hide -1)
      (("1" (inst-cp - "z!1")
        (("1" (inst-cp - "y!1")
          (("1" (inst - "x!1")
            (("1" (skosimp*)
              (("1" (inst-cp - "x!3" "x!4")
                (("1" (inst-cp - "x!2" "x!3")
                  (("1" (inst - "x!2" "x!4")
                    (("1" (inst - "x!2" "x!3" "x!4")
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide -1 -2)
      (("2" (inst-cp - "y!1" "z!1")
        (("2" (inst-cp - "x!1" "y!1")
          (("2" (inst - "x!1" "z!1")
            (("2" (inst - "f!1(x!1)" "f!1(y!1)" "f!1(z!1)")
              (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil isomorphism nil)
    (R formal-type-decl nil isomorphism nil)
    (bijective? const-decl "bool" functions nil)
    (transitive? const-decl "bool" relations nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak))
(isomorphism_preserves_dichotomous 0
  (isomorphism_preserves_dichotomous-1 nil 3315066801
   ("" (grind :if-match nil)
    (("1" (inst-cp - "y!1")
      (("1" (inst - "x!1")
        (("1" (skosimp*)
          (("1" (hide -1)
            (("1" (inst-cp - "x!3" "x!2")
              (("1" (inst - "x!2" "x!3")
                (("1" (inst - "x!2" "x!3") (("1" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide -1 -2)
      (("2" (inst-cp - "y!1" "x!1")
        (("2" (inst - "x!1" "y!1")
          (("2" (inst - "f!1(x!1)" "f!1(y!1)") (("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil isomorphism nil)
    (R formal-type-decl nil isomorphism nil)
    (bijective? const-decl "bool" functions nil)
    (dichotomous? const-decl "bool" orders nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak))
(isomorphism_preserves_trichotomous 0
  (isomorphism_preserves_trichotomous-1 nil 3315066905
   ("" (grind :if-match nil)
    (("1" (inst-cp - "y!1")
      (("1" (inst - "x!1")
        (("1" (skosimp*)
          (("1" (hide -1)
            (("1" (inst-cp - "x!3" "x!2")
              (("1" (inst - "x!2" "x!3")
                (("1" (inst - "x!2" "x!3") (("1" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (inst - "x!1" "y!1")
      (("2" (inst-cp - "y!1" "x!1")
        (("2" (inst - "x!1" "y!1")
          (("2" (inst - "f!1(x!1)" "f!1(y!1)") (("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil isomorphism nil)
    (R formal-type-decl nil isomorphism nil)
    (bijective? const-decl "bool" functions nil)
    (trichotomous? const-decl "bool" orders nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak))
(isomorphism_preserves_well_founded 0
  (isomorphism_preserves_well_founded-1 nil 3315067086
   ("" (skosimp)
    (("" (prop)
      (("1" (grind :if-match nil)
        (("1" (inst -3 "p!1 o f!1")
          (("1" (split)
            (("1" (skolem-typepred)
              (("1" (expand "o")
                (("1" (inst + "f!1(y!2)")
                  (("1" (skolem-typepred)
                    (("1" (inst -5 "x!1")
                      (("1" (skolem!)
                        (("1" (inst - "x!2")
                          (("1" (inst -7 "x!2" "y!2")
                            (("1" (assert) nil nil)) nil)
                           ("2" (expand "o") (("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst - "y!1")
              (("2" (skolem!)
                (("2" (inst + "x!1")
                  (("2" (expand "o") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "isomorphic?")
        (("2" (skolem-typepred)
          (("2" (use "bijective_inverse_exists[D, R]")
            (("2" (expand "exists1")
              (("2" (flatten)
                (("2" (skolem!)
                  (("2" (use "bij_inv_is_bij_alt[D, R]")
                    (("2" (use "comp_inverse_right_alt[D, R]")
                      (("2" (use "comp_inverse_left_alt[D, R]")
                        (("2" (hide -5)
                          (("2" (grind :if-match nil)
                            (("2" (inst -8 "p!1 o x!1")
                              (("2"
                                (split)
                                (("1"
                                  (skolem-typepred)
                                  (("1"
                                    (expand "o")
                                    (("1"
                                      (inst + "x!1(y!2)")
                                      (("1"
                                        (skolem-typepred)
                                        (("1"
                                          (inst -4 "x!2")
                                          (("1"
                                            (inst - "f!1(x!2)")
                                            (("1"
                                              (inst
                                               -12
                                               "x!2"
                                               "x!1(y!2)")
                                              (("1"
                                                (inst - "y!2")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "o")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (inst + "f!1(y!1)")
                                  (("2"
                                    (expand "o")
                                    (("2"
                                      (inst - "y!1")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (pred type-eq-decl nil defined_types nil)
    (p!1 skolem-const-decl "pred[R]" isomorphism nil)
    (f!1 skolem-const-decl "(bijective?[D, R])" isomorphism nil)
    (y!2 skolem-const-decl "(p!1 o f!1)" isomorphism nil)
    (x!2 skolem-const-decl "D" isomorphism nil)
    (injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil isomorphism nil)
    (R formal-type-decl nil isomorphism nil)
    (bijective? const-decl "bool" functions nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (isomorphism? const-decl "bool" isomorphism nil)
    (well_founded? const-decl "bool" orders nil)
    (exists1 const-decl "bool" exists1 nil)
    (comp_inverse_right_alt formula-decl nil function_inverse_def nil)
    (p!1 skolem-const-decl "pred[D]" isomorphism nil)
    (y!2 skolem-const-decl "(p!1 o x!1)" isomorphism nil)
    (x!2 skolem-const-decl "(p!1)" isomorphism nil)
    (comp_inverse_left_alt formula-decl nil function_inverse_def nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (x!1 skolem-const-decl "[R -> D]" isomorphism nil)
    (f!1 skolem-const-decl "(bijective?[D, R])" isomorphism nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil))
   shostak))
(isomorphism_inverse_TCC1 0
  (isomorphism_inverse_TCC1-1 nil 3315829989
   ("" (skosimp* t)
    (("" (expand* "bijective?" "surjective?")
      (("" (flatten) (("" (inst - "r!1") (("" (reduce) nil nil)) nil))
        nil))
      nil))
    nil)
   ((surjective? const-decl "bool" functions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil isomorphism nil)
    (R formal-type-decl nil isomorphism nil)
    (bijective? const-decl "bool" functions nil))
   nil))
(isomorphism_inverse 0
  (isomorphism_inverse-1 nil 3315068744
   ("" (skolem-typepred)
    (("" (prop)
      (("1" (expand* "isomorphism?" "preserves")
        (("1" (skosimp)
          (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (expand* "isomorphism?" "preserves")
        (("2" (skosimp)
          (("2"
            (inst - "inverse_alt(f!1)(x1!1)" "inverse_alt(f!1)(x2!1)")
            (("1" (assert) nil nil)
             ("2" (expand* "bijective?" "surjective?")
              (("2" (flatten)
                (("2" (skolem!)
                  (("2" (inst - "r!1")
                    (("2" (skolem!) (("2" (inst + "x!1") nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (expand* "isomorphism?" "preserves")
        (("3" (skolem!)
          (("3" (prop)
            (("1" (inst - "d1!1" "d2!1") (("1" (assert) nil nil)) nil)
             ("2" (inst -3 "f!1(d1!1)" "f!1(d2!1)")
              (("2" (assert)
                (("2" (expand* "bijective?" "injective?")
                  (("2" (flatten)
                    (("2" (typepred "inverse_alt(f!1)(f!1(d2!1))")
                      (("1" (typepred "inverse_alt(f!1)(f!1(d1!1))")
                        (("1"
                          (inst-cp -6 "inverse_alt(f!1)(f!1(d2!1))"
                           "d2!1")
                          (("1"
                            (inst -6 "inverse_alt(f!1)(f!1(d1!1))"
                             "d1!1")
                            (("1" (assert) nil nil)
                             ("2" (flatten) (("2" (inst?) nil nil))
                              nil))
                            nil)
                           ("2" (flatten) (("2" (inst?) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (flatten) (("2" (inst?) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((isomorphism? const-decl "bool" isomorphism nil)
    (preserves const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (bijective_inverse_alt_is_bijective application-judgement
     "(bijective?[R, D])" function_inverse_alt nil)
    (unique_bijective_inverse_alt application-judgement
     "{d | f(d) = r}" function_inverse_alt nil)
    (inverse_alt const-decl "inverses(f)" function_inverse_alt nil)
    (inverses nonempty-type-eq-decl nil function_inverse_alt nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (FALSE const-decl "bool" booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (injective? const-decl "bool" functions nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bijective? const-decl "bool" functions nil)
    (R formal-type-decl nil isomorphism nil)
    (D formal-type-decl nil isomorphism nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.