Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: relation_choice_properties.prf Sprache: Lisp

Original von: PVS^©

(relational_choice_properties
(fun_choice_impl_description 0
  (fun_choice_impl_description-1 nil 3569913521 ("" (grind) nil nil)
   ((parametric_definite_description const-decl "bool"
     relational_choice nil)
    (fun_choice const-decl "bool" relational_choice nil)
    (T formal-nonempty-type-decl nil relational_choice_properties nil)
    (U formal-nonempty-type-decl nil relational_choice_properties nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil))
   shostak))
(fun_choice_impl_rel_unique_choice 0
  (fun_choice_impl_rel_unique_choice-1 nil 3569913791
   ("" (flatten)
    (("" (expand "fun_choice")
      (("" (expand "rel_unique_choice")
        (("" (skolem! 1)
          (("" (inst -1 "R!1")
            (("" (flatten)
              (("" (prop)
                (("" (skolem-typepred)
                  (("" (inst 1 "LAMBDA(t:T,u:U):u=f!1(t)")
                    (("" (skolem-typepred)
                      (("" (inst 1 "f!1(t!1)")
                        (("" (split)
                          (("1" (inst -1 "t!1") nil nil)
                           ("2" (inst?)
                            (("2" (skolem! 1)
                              (("2"
                                (prop)
                                (("2"
                                  (replace -1 1 rl)
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((fun_choice const-decl "bool" relational_choice nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (U formal-nonempty-type-decl nil relational_choice_properties nil)
    (T formal-nonempty-type-decl nil relational_choice_properties nil)
    (rel_unique_choice const-decl "bool" relational_choice nil))
   shostak))
(fun_choice_impl_rel_choice 0
  (fun_choice_impl_rel_choice-1 nil 3569913534
   ("" (flatten)
    (("" (auto-rewrite-defs :always? t)
      ((""
        (assert :let-reduce? t :cases-rewrite? nil :ignore-typepreds?
                nil)
        (("" (skolem-typepred)
          (("" (flatten)
            ((""
              (assert :let-reduce? t :quant-simp? nil
                      :implicit-typepreds? nil :ignore-typepreds? nil
                      :cases-rewrite? nil)
              (("" (inst? :if-match t :polarity? nil)
                (("" (replace*)
                  ((""
                    (assert :let-reduce? t :quant-simp? nil
                            :implicit-typepreds? nil :ignore-typepreds?
                            nil :cases-rewrite? nil)
                    (("" (inst? :if-match t :polarity? nil)
                      (("" (skolem-typepred)
                        (("" (replace*)
                          ((""
                            (assert :let-reduce? t :quant-simp? nil
                                    :implicit-typepreds? nil
                                    :ignore-typepreds? nil
                                    :cases-rewrite? nil)
                            (("" (skolem-typepred)
                              (("" (flatten) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (U formal-nonempty-type-decl nil relational_choice_properties nil)
    (T formal-nonempty-type-decl nil relational_choice_properties nil)
    (fun_choice const-decl "bool" relational_choice nil)
    (\|- const-decl "bool" relation_implication nil)
    (rel_choice const-decl "bool" relational_choice nil))
   shostak))
(fun_choice_impl_rel_choice_impl_description_rel_choice 0
  (fun_choice_impl_rel_choice_impl_description_rel_choice-1 nil
   3569927551
   ("" (flatten)
    (("" (expand "parametric_definite_description")
      (("" (expand "rel_choice")
        (("" (expand "fun_choice")
          (("" (skosimp*) (("" (grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((parametric_definite_description const-decl "bool"
     relational_choice nil)
    (fun_choice const-decl "bool" relational_choice nil)
    (\|- const-decl "bool" relation_implication nil)
    (T formal-nonempty-type-decl nil relational_choice_properties nil)
    (U formal-nonempty-type-decl nil relational_choice_properties nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (rel_choice const-decl "bool" relational_choice nil))
   shostak))
(fun_choice_impl_rel_choice_and_description_rel_choice 0
  (fun_choice_impl_rel_choice_and_description_rel_choice-1 nil
   3569927629
   ("" (flatten)
    (("" (prop)
      (("1" (rewrite "fun_choice_impl_rel_choice") nil nil)
       ("2" (rewrite "fun_choice_impl_description") nil nil))
      nil))
    nil)
   ((fun_choice_impl_rel_choice formula-decl nil
     relational_choice_properties nil)
    (fun_choice_impl_description formula-decl nil
     relational_choice_properties nil))
   shostak))
(fun_choice_impl_rel_unique_choice_impl_description_rel_choice 0
  (fun_choice_impl_rel_unique_choice_impl_description_rel_choice-1 nil
   3569913544 ("" (grind) nil nil)
   ((parametric_definite_description const-decl "bool"
     relational_choice nil)
    (rel_unique_choice const-decl "bool" relational_choice nil)
    (fun_choice const-decl "bool" relational_choice nil)
    (T formal-nonempty-type-decl nil relational_choice_properties nil)
    (U formal-nonempty-type-decl nil relational_choice_properties nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil))
   shostak))
(fun_choice_impl_rel_unique_choice_and_description_rel_choice 0
  (fun_choice_impl_rel_unique_choice_and_description_rel_choice-1 nil
   3569913565
   ("" (flatten)
    (("" (prop)
      (("1" (rewrite "fun_choice_impl_rel_unique_choice") nil nil)
       ("2" (rewrite "fun_choice_impl_description") nil nil))
      nil))
    nil)
   ((fun_choice_impl_rel_unique_choice formula-decl nil
     relational_choice_properties nil)
    (fun_choice_impl_description formula-decl nil
     relational_choice_properties nil))
   shostak))
(description_rel_unique_choice_imp_funct_choice 0
  (description_rel_unique_choice_imp_funct_choice-1 nil 3569929474
   ("" (prop)
    (("" (expand "fun_choice")
      (("" (skosimp*)
        (("" (expand "rel_unique_choice")
          (("" (inst -2 "R!1")
            (("" (prop)
              (("" (skolem!)
                (("" (expand "parametric_definite_description")
                  (("" (inst -2 "R1!1")
                    (("" (prop)
                      (("1" (skolem! -1)
                        (("1" (inst 1 "f!1")
                          (("1" (skolem! 1)
                            (("1" (inst -1 "t!1")
                              (("1"
                                (inst -2 "t!1")
                                (("1"
                                  (skolem!)
                                  (("1"
                                    (prop)
                                    (("1"
                                      (inst -4 "f!1(t!1)")
                                      (("1"
                                        (prop)
                                        (("1"
                                          (replace -1 1 rl)
                                          (("1" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (inst?)
                          (("2" (skolem!)
                            (("2" (prop)
                              (("2"
                                (inst 1 "u!1")
                                (("2" (prop) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((fun_choice const-decl "bool" relational_choice nil)
    (rel_unique_choice const-decl "bool" relational_choice nil)
    (parametric_definite_description const-decl "bool"
     relational_choice nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (U formal-nonempty-type-decl nil relational_choice_properties nil)
    (T formal-nonempty-type-decl nil relational_choice_properties nil))
   shostak))
(description_rel_and_rel_unique_choice_imp_funct_choice 0
  (description_rel_and_rel_unique_choice_imp_funct_choice-1 nil
   3569927488
   ("" (flatten)
    (("" (rewrite "description_rel_unique_choice_imp_funct_choice") nil
      nil))
    nil)
   ((description_rel_unique_choice_imp_funct_choice formula-decl nil
     relational_choice_properties nil))
   shostak))
(rel_choice_and_proof_irrel_imp_guarded_rel_choice 0
  (rel_choice_and_proof_irrel_imp_guarded_rel_choice-1 nil 3570044635
   ("" (flatten)
    (("" (expand "conditional_relational_choice")
      (("" (expand "proof_irrelevance")
        (("" (expand "rel_unique_choice")
          (("" (skolem!)
            (("" (skolem!)
              (("" (prop)
                (("" (inst -1 "R!1")
                  (("" (prop)
                    (("1" (skolem!)
                      (("1" (inst 1 "R1!1")
                        (("1" (skolem!)
                          (("1" (inst?) (("1" (flatten) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (inst 2 "R!1")
                      (("2" (skolem!)
                        (("2" (skolem!)
                          (("2" (bddsimp)
                            (("2" (assert)
                              (("2"
                                (inst?)
                                (("2"
                                  (replace 1 -1 rl)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (inst -1 "P!1(t!2)")
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((conditional_relational_choice const-decl "bool" relational_choice
     nil)
    (rel_unique_choice const-decl "bool" relational_choice nil)
    (T formal-nonempty-type-decl nil relational_choice_properties nil)
    (U formal-nonempty-type-decl nil relational_choice_properties nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (proof_irrelevance const-decl "bool" relational_choice nil))
   shostak))
(relx_choice_indep_of_premises_imp_guarded_rel_choice 0
  (relx_choice_indep_of_premises_imp_guarded_rel_choice-1 nil
   3570114627
   ("" (flatten)
    (("" (expand "conditional_relational_choice")
      (("" (skolem! 1)
        (("" (skolem! 1)
          (("" (prop)
            (("" (expand "rel_unique_choice")
              (("" (inst -1 "LAMBDA(t:T,u:U):P!1(t) IMPLIES R!1(t,u)")
                (("" (prop)
                  (("1" (skolem!)
                    (("1" (inst 1 "R1!1")
                      (("1" (skolem! 1)
                        (("1" (prop)
                          (("1" (inst?)
                            (("1" (skolem!)
                              (("1"
                                (prop)
                                (("1"
                                  (inst 1 "u!1")
                                  (("1" (prop) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "independence_of_premises")
                    (("2" (inst -1 "P!1")
                      (("2" (skolem! 1)
                        (("2" (inst -1 "P!1(t!1)")
                          (("2" (prop)
                            (("1" (assert)
                              (("1"
                                (inst?)
                                (("1"
                                  (prop)
                                  (("1"
                                    (inst 2 "R!1")
                                    (("1"
                                      (skolem!)
                                      (("1"
                                        (skolem!)
                                        (("1"
                                          (inst?)
                                          (("1" (prop) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (inst 3 "R!1")
                                    (("2"
                                      (skolem! 3)
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (skolem!)
                                          (("2"
                                            (prop)
                                            (("1" (assert) nil nil)
                                             ("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (inst 1 "t!1") nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((conditional_relational_choice const-decl "bool" relational_choice
     nil)
    (rel_unique_choice const-decl "bool" relational_choice nil)
    (independence_of_premises const-decl "bool" relational_choice nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (U formal-nonempty-type-decl nil relational_choice_properties nil)
    (T formal-nonempty-type-decl nil relational_choice_properties nil))
   shostak))
(fun_choice_equiv_rel_unique_param_desc 0
  (fun_choice_equiv_rel_unique_param_desc-1 nil 3569914637
   ("" (prop)
    (("1" (rewrite "fun_choice_impl_rel_unique_choice") nil nil)
     ("2" (rewrite "fun_choice_impl_description") nil nil)
     ("3" (rewrite "description_rel_unique_choice_imp_funct_choice")
      nil nil))
    nil)
   ((description_rel_unique_choice_imp_funct_choice formula-decl nil
     relational_choice_properties nil)
    (fun_choice_impl_description formula-decl nil
     relational_choice_properties nil)
    (fun_choice_impl_rel_unique_choice formula-decl nil
     relational_choice_properties nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.28 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.