Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: basis.prf Sprache: Lisp

Original von: PVS^©

(basis
(synthetic_generated_def 0
  (synthetic_generated_def-1 nil 3325600227
   ("" (skosimp)
    (("" (expand "member")
      (("" (expand "synthetic_generated_topology_set")
        (("" (propax) nil nil)) nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (synthetic_generated_topology_set const-decl "setofsets[T]" basis
     nil))
   shostak))
(synthetic_generated_alt_def 0
  (synthetic_generated_alt_def-1 nil 3327203368
   ("" (skosimp)
    (("" (typepred "B!1")
      (("" (expand "member")
        (("" (expand "extend")
          (("" (expand "synthetic_generated_topology_set")
            (("" (split 1)
              (("1" (flatten)
                (("1" (apply-extensionality :hide? t)
                  (("1" (expand "Union" 1)
                    (("1" (case-replace "A!1(x!1)")
                      (("1" (skosimp)
                        (("1" (replace -3 -1 rl)
                          (("1" (expand "Union")
                            (("1" (skosimp)
                              (("1"
                                (typepred "a!1")
                                (("1"
                                  (inst + "a!1")
                                  (("1"
                                    (expand "subset?")
                                    (("1"
                                      (inst - "a!1")
                                      (("1"
                                        (expand "member")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (replace -5 1 rl)
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (inst + "a!1")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (replace 1 2)
                        (("2" (assert)
                          (("2" (skosimp*)
                            (("2" (typepred "a!1")
                              (("2"
                                (assert)
                                (("2"
                                  (expand "subset?")
                                  (("2"
                                    (inst - "x!1")
                                    (("2"
                                      (expand "member")
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (flatten)
                (("2"
                  (inst +
                   "extend[setof[T],(B!1),bool,FALSE]({x:(B!1)|subset?(x, A!1)})")
                  (("2" (split 1)
                    (("1" (expand "subset?")
                      (("1" (skosimp)
                        (("1" (expand "extend")
                          (("1" (expand "member")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "extend")
                      (("2" (replace -1 1 rl) (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((synthetic_base type-eq-decl nil basis nil)
    (synthetic_base? const-decl "bool" basis nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil basis nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (subset? const-decl "bool" sets nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (Union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (B!1 skolem-const-decl "synthetic_base" basis nil)
    (V!1 skolem-const-decl "setofsets[T]" basis nil)
    (a!1 skolem-const-decl "(V!1)" basis nil)
    (A!1 skolem-const-decl "set[T]" basis nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (synthetic_generated_topology_set const-decl "setofsets[T]" basis
     nil)
    (member const-decl "bool" sets nil))
   shostak))
(synthetic_generated_empty 0
  (synthetic_generated_empty-1 nil 3327203925
   ("" (skosimp)
    (("" (typepred "B!1")
      (("" (expand "synthetic_generated_topology_set")
        (("" (expand "emptyset")
          (("" (expand "member")
            (("" (inst + "emptyset[set[T]]")
              (("" (split 1)
                (("1" (expand "subset?")
                  (("1" (skosimp)
                    (("1" (expand "emptyset")
                      (("1" (expand "member") (("1" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (apply-extensionality 1 :hide? t)
                  (("2" (expand "emptyset")
                    (("2" (expand "Union") (("2" (skosimp) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((synthetic_base type-eq-decl nil basis nil)
    (synthetic_base? const-decl "bool" basis nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil basis nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil) (Union const-decl "set" sets nil)
    (FALSE const-decl "bool" booleans nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (synthetic_generated_topology_set const-decl "setofsets[T]" basis
     nil))
   shostak))
(synthetic_generated_full 0
  (synthetic_generated_full-1 nil 3327203995
   ("" (skosimp)
    (("" (typepred "B!1")
      (("" (expand "synthetic_base?")
        (("" (flatten)
          (("" (expand "synthetic_generated_topology_set")
            (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((synthetic_base type-eq-decl nil basis nil)
    (synthetic_base? const-decl "bool" basis nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil basis 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)
    (synthetic_generated_topology_set const-decl "setofsets[T]" basis
     nil))
   shostak))
(synthetic_generated_Union 0
  (synthetic_generated_Union-1 nil 3325507747
   ("" (expand "topology_Union?")
    (("" (skosimp*)
      (("" (rewrite "synthetic_generated_alt_def" 1)
        (("" (apply-extensionality 1 :hide? t)
          (("" (case-replace "Union(U!1)(x!1)")
            (("1" (expand "Union" -1)
              (("1" (expand "Union" 1 1)
                (("1" (skosimp)
                  (("1" (typepred "a!1")
                    (("1" (expand "subset?" -3)
                      (("1" (inst-cp - "a!1")
                        (("1" (expand "member" -4 1)
                          (("1"
                            (rewrite "synthetic_generated_alt_def" -4)
                            (("1" (replace -4 -2)
                              (("1"
                                (expand "Union" -2)
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (typepred "a!2")
                                    (("1"
                                      (expand "extend")
                                      (("1"
                                        (case-replace "B!1(a!2)")
                                        (("1"
                                          (inst + "a!2")
                                          (("1"
                                            (expand "extend")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (expand "subset?")
                                                (("1"
                                                  (skosimp)
                                                  (("1"
                                                    (expand "member")
                                                    (("1"
                                                      (expand "Union")
                                                      (("1"
                                                        (inst - "x!2")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (inst
                                                             +
                                                             "a!1")
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (replace 1 2)
              (("2" (assert)
                (("2" (expand "extend")
                  (("2" (expand "Union")
                    (("2" (skosimp)
                      (("2" (typepred "a!1")
                        (("2" (assert)
                          (("2" (expand "subset?")
                            (("2" (inst - "x!1")
                              (("2"
                                (expand "member")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (B!1 skolem-const-decl "synthetic_base" basis nil)
    (U!1 skolem-const-decl "setofsets[T]" basis nil)
    (a!1 skolem-const-decl "(U!1)" basis nil)
    (a!2 skolem-const-decl
     "(extend[setof[T], (B!1), bool, FALSE]({x: (B!1) | subset?(x, a!1)}))"
     basis nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (synthetic_base type-eq-decl nil basis nil)
    (synthetic_base? const-decl "bool" basis nil)
    (Union const-decl "set" sets nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types 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 basis nil)
    (synthetic_generated_alt_def formula-decl nil basis nil)
    (topology_Union? const-decl "bool" topology_prelim nil))
   shostak))
(synthetic_generated_intersection 0
  (synthetic_generated_intersection-1 nil 3325507689
   ("" (skolem 1 ("B"))
    (("" (expand "topology_intersection?")
      (("" (skosimp*)
        (("" (typepred "A!1")
          (("" (typepred "B!1")
            (("" (rewrite "synthetic_generated_def" 1)
              ((""
                (lemma "synthetic_generated_alt_def"
                 ("B" "B" "A" "A!1"))
                ((""
                  (lemma "synthetic_generated_alt_def"
                   ("B" "B" "A" "B!1"))
                  (("" (expand "member")
                    ((""
                      (inst +
                       "{z:(B) | subset?(z,A!1) & subset?(z,B!1)}")
                      (("" (split 1)
                        (("1" (expand "extend")
                          (("1" (expand "subset?")
                            (("1" (skosimp)
                              (("1"
                                (expand "member")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (apply-extensionality 1 :hide? t)
                          (("2"
                            (case-replace
                             "intersection(A!1, B!1)(x!1)")
                            (("1" (expand "intersection")
                              (("1"
                                (expand "member")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (expand "extend")
                                    (("1"
                                      (expand "Union")
                                      (("1"
                                        (replace -3 -2)
                                        (("1"
                                          (replace -4 -1)
                                          (("1"
                                            (hide -3 -4)
                                            (("1"
                                              (assert)
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (typepred "a!1")
                                                  (("1"
                                                    (typepred "a!2")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (typepred "B")
                                                        (("1"
                                                          (expand
                                                           "synthetic_base?")
                                                          (("1"
                                                            (flatten)
                                                            (("1"
                                                              (hide -1)
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "a!1"
                                                                 "a!2")
                                                                (("1"
                                                                  (skosimp)
                                                                  (("1"
                                                                    (lemma
                                                                     "extensionality_postulate"
                                                                     ("f"
                                                                      "Union(V!1)"
                                                                      "g"
                                                                      "intersection(a!1, a!2)"))
                                                                    (("1"
                                                                      (flatten
                                                                       -1)
                                                                      (("1"
                                                                        (hide
                                                                         -1)
                                                                        (("1"
                                                                          (split
                                                                           -1)
                                                                          (("1"
                                                                            (inst
                                                                             -
                                                                             "x!1")
                                                                            (("1"
                                                                              (expand
                                                                               "intersection"
                                                                               -1)
                                                                              (("1"
                                                                                (expand
                                                                                 "member")
                                                                                (("1"
                                                                                  (expand
                                                                                   "Union"
                                                                                   -1)
                                                                                  (("1"
                                                                                    (skosimp)
                                                                                    (("1"
                                                                                      (typepred
                                                                                       "a!3")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "subset?")
                                                                                        (("1"
                                                                                          (inst
                                                                                           -3
                                                                                           "a!3")
                                                                                          (("1"
                                                                                            (expand
                                                                                             "member")
                                                                                            (("1"
                                                                                              (inst
                                                                                               +
                                                                                               "a!3")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (lemma
                                                                                                   "Union_subset"
                                                                                                   ("A"
                                                                                                    "V!1"
                                                                                                    "a"
                                                                                                    "a!3"))
                                                                                                  (("1"
                                                                                                    (replace
                                                                                                     -5
                                                                                                     -1)
                                                                                                    (("1"
                                                                                                      (hide-all-but
                                                                                                       (-1
                                                                                                        -6
                                                                                                        -8
                                                                                                        1))
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "intersection")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "subset?")
                                                                                                          (("1"
                                                                                                            (expand
                                                                                                             "member")
                                                                                                            (("1"
                                                                                                              (split
                                                                                                               1)
                                                                                                              (("1"
                                                                                                                (skosimp)
                                                                                                                (("1"
                                                                                                                  (inst
                                                                                                                   -
                                                                                                                   "x!2")
                                                                                                                  (("1"
                                                                                                                    (assert)
                                                                                                                    (("1"
                                                                                                                      (flatten)
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -5
                                                                                                                         "x!2")
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil)
                                                                                                               ("2"
                                                                                                                (skosimp)
                                                                                                                (("2"
                                                                                                                  (inst
                                                                                                                   -
                                                                                                                   "x!2")
                                                                                                                  (("2"
                                                                                                                    (assert)
                                                                                                                    (("2"
                                                                                                                      (flatten)
                                                                                                                      (("2"
                                                                                                                        (inst
                                                                                                                         -
                                                                                                                         "x!2")
                                                                                                                        (("2"
                                                                                                                          (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)
                                                                           ("2"
                                                                            (propax)
                                                                            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" (replace 1 2)
                              (("2"
                                (assert)
                                (("2"
                                  (expand "extend")
                                  (("2"
                                    (expand "Union")
                                    (("2"
                                      (skosimp)
                                      (("2"
                                        (typepred "a!1")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (flatten)
                                            (("2"
                                              (expand "intersection")
                                              (("2"
                                                (expand "subset?")
                                                (("2"
                                                  (inst - "x!1")
                                                  (("2"
                                                    (inst - "x!1")
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (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)
   ((topology_intersection? const-decl "bool" topology_prelim nil)
    (synthetic_generated_topology_set const-decl "setofsets[T]" basis
     nil)
    (synthetic_base type-eq-decl nil basis nil)
    (synthetic_base? const-decl "bool" basis nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil basis nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (synthetic_generated_def formula-decl nil basis nil)
    (set type-eq-decl nil sets nil)
    (intersection const-decl "set" sets nil)
    (subset? const-decl "bool" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (Union const-decl "set" sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (B skolem-const-decl "synthetic_base" basis nil)
    (V!1 skolem-const-decl "setofsets[T]" basis nil)
    (a!3 skolem-const-decl "(V!1)" basis nil)
    (A!1 skolem-const-decl "(synthetic_generated_topology_set(B))"
     basis nil)
    (B!1 skolem-const-decl "(synthetic_generated_topology_set(B))"
     basis nil)
    (Union_subset formula-decl nil sets_lemmas nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (extensionality_postulate formula-decl nil functions nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (synthetic_generated_alt_def formula-decl nil basis nil))
   shostak))
(synthetic_generated_topology_TCC1 0
  (synthetic_generated_topology_TCC1-1 nil 3325474953
   ("" (skosimp)
    (("" (expand "topology?")
      (("" (split)
        (("1" (lemma "synthetic_generated_empty")
          (("1" (inst - "B!1")
            (("1" (expand "topology_empty?")
              (("1" (expand "synthetic_generated_topology_set")
                (("1" (propax) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (expand "topology_full?")
          (("2" (lemma "synthetic_generated_full" ("B" "B!1"))
            (("2" (expand "synthetic_generated_topology_set")
              (("2" (propax) nil nil)) nil))
            nil))
          nil)
         ("3" (lemma "synthetic_generated_Union" ("B" "B!1"))
          (("3" (expand "synthetic_generated_topology_set")
            (("3" (propax) nil nil)) nil))
          nil)
         ("4" (lemma "synthetic_generated_intersection" ("B" "B!1"))
          (("4" (expand "synthetic_generated_topology_set")
            (("4" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((topology? const-decl "bool" topology_prelim nil)
    (synthetic_generated_intersection formula-decl nil basis nil)
    (synthetic_generated_Union formula-decl nil basis nil)
    (topology_full? const-decl "bool" topology_prelim nil)
    (synthetic_generated_full formula-decl nil basis nil)
    (synthetic_generated_empty formula-decl nil basis nil)
    (topology_empty? const-decl "bool" topology_prelim nil)
    (synthetic_generated_topology_set const-decl "setofsets[T]" basis
     nil)
    (synthetic_base type-eq-decl nil basis nil)
    (synthetic_base? const-decl "bool" basis nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil basis nil))
   shostak))
(synthetic_basis_is_topology 0
  (synthetic_basis_is_topology-1 nil 3333943016
   ("" (skosimp)
    ((""
      (case-replace
       "synthetic_generated_topology_set(B!1) = synthetic_generated_topology(B!1)")
      (("1" (typepred "synthetic_generated_topology(B!1)")
        (("1" (propax) nil nil)) nil)
       ("2" (hide 2)
        (("2" (expand "synthetic_generated_topology_set")
          (("2" (expand "synthetic_generated_topology")
            (("2" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil basis nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (synthetic_base? const-decl "bool" basis nil)
    (synthetic_base type-eq-decl nil basis nil)
    (synthetic_generated_topology_set const-decl "setofsets[T]" basis
     nil)
    (topology? const-decl "bool" topology_prelim nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (synthetic_generated_topology const-decl "topology" basis nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   shostak))
(base_is_synthetic_base 0
  (base_is_synthetic_base-1 nil 3345995725
   ("" (skosimp)
    (("" (expand "base?")
      (("" (expand "synthetic_base?")
        (("" (flatten)
          (("" (split 1)
            (("1" (typepred "t!1")
              (("1" (expand "topology?")
                (("1" (flatten)
                  (("1" (expand "topology_full?")
                    (("1" (expand "member")
                      (("1" (inst - "fullset[T]") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp)
              (("2" (typepred "B1!1")
                (("2" (typepred "B2!1")
                  (("2" (typepred "t!1")
                    (("2" (expand "topology?")
                      (("2" (flatten)
                        (("2" (expand "subset?" -7)
                          (("2" (inst-cp - "B1!1")
                            (("2" (inst - "B2!1")
                              (("2"
                                (expand "member")
                                (("2"
                                  (expand "topology_intersection?")
                                  (("2"
                                    (inst - "B1!1" "B2!1")
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (inst
                                         -
                                         "intersection(B1!1, B2!1)")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((base? const-decl "bool" basis nil)
    (subset? const-decl "bool" sets nil)
    (topology_intersection? const-decl "bool" topology_prelim nil)
    (intersection const-decl "set" sets nil)
    (B2!1 skolem-const-decl "(U!1)" basis nil)
    (B1!1 skolem-const-decl "(U!1)" basis nil)
    (U!1 skolem-const-decl "setofsets[T]" basis nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (topology? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil basis 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)
    (t!1 skolem-const-decl "topology[T]" basis nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
    (topology_full? const-decl "bool" topology_prelim nil)
    (synthetic_base? const-decl "bool" basis nil))
   shostak))
(synthetic_base_is_base 0
  (synthetic_base_is_base-1 nil 3345996105
   ("" (skosimp)
    (("" (typepred "B!1")
      (("" (expand "base?")
        (("" (split 1)
          (("1" (expand "subset?")
            (("1" (skosimp)
              (("1" (expand "member")
                (("1" (expand "synthetic_generated_topology_set")
                  (("1" (expand "synthetic_base?")
                    (("1" (flatten)
                      (("1" (inst -3 "x!1" "x!1")
                        (("1" (hide -2)
                          (("1" (rewrite "intersection_idempotent") nil
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (skosimp)
            (("2" (typepred "A!1")
              (("2" (expand "synthetic_generated_topology_set")
                (("2" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((synthetic_base type-eq-decl nil basis nil)
    (synthetic_base? const-decl "bool" basis nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil basis nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (synthetic_generated_topology_set const-decl "setofsets[T]" basis
     nil)
    (intersection_idempotent formula-decl nil sets_lemmas nil)
    (set type-eq-decl nil sets nil)
    (x!1 skolem-const-decl "setof[T]" basis nil)
    (B!1 skolem-const-decl "synthetic_base" basis nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (base? const-decl "bool" basis nil))
   shostak)))

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