Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: fp_round_aux.prf Sprache: Lisp

Original von: PVS^©

(continuation
(IMP_fixpoints_TCC1 0
  (IMP_fixpoints_TCC1-1 nil 3353544462
   ("" (inst + "I[Cont]")
    (("" (assert)
      (("" (expand "scott_continuous?")
        (("" (split)
          (("1" (expand "increasing?")
            (("1" (skosimp)
              (("1" (expand "I") (("1" (propax) nil nil)) nil)) nil))
            nil)
           ("2" (expand "lub_preserving?")
            (("2" (skosimp*)
              (("2" (expand "I")
                (("2" (expand "image")
                  (("2"
                    (case-replace
                     "{y: Cont | EXISTS (x_1: (D!1)): y = x_1} = D!1")
                    (("2" (apply-extensionality 1 :hide? t)
                      (("2" (case-replace "D!1(x!1)")
                        (("1" (inst + "x!1") nil nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((I const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (scott_continuous type-eq-decl nil scott_continuity "scott/")
    (scott_continuous? const-decl "bool" scott_continuity "scott/")
    (sq_le const-decl "bool" Cont nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Cont nonempty-type-eq-decl nil Cont nil)
    (lift type-decl nil lift_adt nil)
    (State nonempty-type-eq-decl nil State 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)
    (V formal-nonempty-type-decl nil continuation nil)
    (I_is_continuous name-judgement "continuous
    [Cont, scott_open_sets[Cont, (sq_le)], Cont,
     scott_open_sets[Cont, (sq_le)]]" continuation nil))
   nil))
(identity_continuous 0
  (identity_continuous-1 nil 3353548340
   ("" (expand "I")
    (("" (expand "scott_continuous?")
      (("" (split)
        (("1" (expand "increasing?") (("1" (skosimp) nil nil)) nil)
         ("2" (expand "lub_preserving?")
          (("2" (skosimp)
            (("2" (typepred "D!1")
              (("2" (expand "image")
                (("2"
                  (case-replace
                   "{y: Cont | EXISTS (x_1: (D!1)): y = x_1}=D!1")
                  (("2" (hide 2)
                    (("2" (apply-extensionality 1 :hide? t)
                      (("2" (case-replace "D!1(x!1)")
                        (("1" (inst + "x!1") nil nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((scott_continuous? const-decl "bool" scott_continuity "scott/")
    (lub_preserving? const-decl "bool" scott_continuity "scott/")
    (directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (sq_le const-decl "bool" Cont nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (Cont nonempty-type-eq-decl nil Cont nil)
    (lift type-decl nil lift_adt nil)
    (State nonempty-type-eq-decl nil State 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)
    (number nonempty-type-decl nil numbers nil)
    (V formal-nonempty-type-decl nil continuation nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (D!1 skolem-const-decl "directed[Cont[V], (sq_le)]" continuation
     nil)
    (x!1 skolem-const-decl "[[V -> int] -> lift[State[V]]]"
     continuation nil)
    (image const-decl "set[R]" function_image nil)
    (increasing? const-decl "bool" fun_preds_partial "scott/")
    (I const-decl "(bijective?[T, T])" identity nil))
   shostak))
(composition_continuous 0
  (composition_continuous-1 nil 3353645372
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (typepred "g!1")
        (("" (expand "scott_continuous?")
          (("" (flatten)
            (("" (expand "o ")
              (("" (split)
                (("1" (expand "increasing?")
                  (("1" (skosimp)
                    (("1" (inst - "x!1" "y!1")
                      (("1" (assert)
                        (("1" (inst - "g!1(x!1)" "g!1(y!1)")
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "lub_preserving?")
                  (("2" (skosimp)
                    (("2" (typepred "D!1")
                      (("2" (inst - "D!1")
                        (("2"
                          (lemma "lub_set_image" ("g" "g!1" "D" "D!1"))
                          (("1" (assert)
                            (("1" (replace -6)
                              (("1"
                                (inst - "image(g!1,D!1)")
                                (("1"
                                  (split -8)
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (case-replace
                                       "image(LAMBDA (x: Cont): f!1(g!1(x)), D!1) = image(f!1, image(g!1, D!1))")
                                      (("1"
                                        (hide-all-but 1)
                                        (("1"
                                          (expand "image")
                                          (("1"
                                            (apply-extensionality
                                             1
                                             :hide?
                                             t)
                                            (("1"
                                              (case-replace
                                               "(EXISTS (x_1: (D!1)): x!1 = f!1(g!1(x_1)))")
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (inst + "g!1(x!2)")
                                                  (("1"
                                                    (inst + "x!2")
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (replace 1 2)
                                                (("2"
                                                  (assert)
                                                  (("2"
                                                    (skosimp)
                                                    (("2"
                                                      (typepred "x!2")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (replace -1)
                                                          (("2"
                                                            (replace
                                                             -2)
                                                            (("2"
                                                              (hide-all-but
                                                               1)
                                                              (("2"
                                                                (inst
                                                                 +
                                                                 "x!3")
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (case-replace
                                     "image(LAMBDA (x: Cont): f!1(g!1(x)), D!1) = image(f!1, image(g!1, D!1))")
                                    (("2"
                                      (hide-all-but 1)
                                      (("2"
                                        (expand "image")
                                        (("2"
                                          (apply-extensionality
                                           1
                                           :hide?
                                           t)
                                          (("2"
                                            (case-replace
                                             "(EXISTS (x_1: (D!1)): x!1 = f!1(g!1(x_1)))")
                                            (("1"
                                              (skosimp)
                                              (("1"
                                                (inst + "g!1(x!2)")
                                                (("1"
                                                  (inst + "x!2")
                                                  nil
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (replace 1 2)
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (typepred "x!2")
                                                    (("2"
                                                      (skosimp)
                                                      (("2"
                                                        (inst + "x!3")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (lemma
                                   "directed_image"
                                   ("g" "g!1" "D" "D!1"))
                                  (("2"
                                    (assert)
                                    (("2"
                                      (hide-all-but (-3 1))
                                      (("2"
                                        (expand "image")
                                        (("2"
                                          (expand "nonempty?")
                                          (("2"
                                            (expand "empty?")
                                            (("2"
                                              (expand "member")
                                              (("2"
                                                (skosimp*)
                                                (("2"
                                                  (inst - "g!1(x!1)")
                                                  (("2"
                                                    (inst + "x!1")
                                                    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)
   ((scott_continuous type-eq-decl nil scott_continuity "scott/")
    (scott_continuous? const-decl "bool" scott_continuity "scott/")
    (sq_le const-decl "bool" Cont nil)
    (Cont nonempty-type-eq-decl nil Cont nil)
    (lift type-decl nil lift_adt nil)
    (State nonempty-type-eq-decl nil State 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)
    (number nonempty-type-decl nil numbers nil)
    (V formal-nonempty-type-decl nil continuation nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (composition_is_continuous application-judgement "continuous
    [Cont, scott_open_sets[Cont, (sq_le)], Cont,
     scott_open_sets[Cont, (sq_le)]]" continuation nil)
    (O const-decl "T3" function_props nil)
    (lub_preserving? const-decl "bool" scott_continuity "scott/")
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (directed? const-decl "bool" directed_order_props "orders/")
    (directed type-eq-decl nil directed_order_props "orders/")
    (lub_set_image formula-decl nil scott_continuity "scott/")
    (directed_image formula-decl nil scott_continuity "scott/")
    (member const-decl "bool" sets nil)
    (x!1 skolem-const-decl "Cont[V]" continuation nil)
    (empty? const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (x!2 skolem-const-decl "(D!1)" continuation nil)
    (x!2 skolem-const-decl "(D!1)" continuation nil)
    (D!1 skolem-const-decl "directed[Cont, (sq_le)]" continuation nil)
    (g!1 skolem-const-decl
     "scott_continuous[Cont, Cont, (sq_le), (sq_le)]" continuation nil)
    (image const-decl "set[R]" function_image nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (increasing? const-decl "bool" fun_preds_partial "scott/")
    (sq_le_pdcpo name-judgement
     "(pointed_directed_complete_partial_order?[Cont])" continuation
     nil))
   shostak))
(assign_continuous 0
  (assign_continuous-1 nil 3354465346
   ("" (skosimp)
    (("" (expand "assign")
      (("" (expand "assign")
        (("" (lemma "Cont.apply_continuous")
          ((""
            (inst -
             "(LAMBDA s: up(lambda (y:V): IF y = x!1 THEN A(a!1)(s) ELSE s(y) ENDIF))")
            (("" (expand "o") (("" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((assign const-decl "State" State nil)
    (V formal-nonempty-type-decl nil continuation nil)
    (apply_continuous formula-decl nil Cont nil)
    (O const-decl "LiftPartialFunction[X, Z]"
     PartialFunctionComposition nil)
    (A def-decl "[State -> int]" AExp nil)
    (AExp type-decl nil AExp nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (Cont nonempty-type-eq-decl nil Cont nil)
    (lift type-decl nil lift_adt nil)
    (State nonempty-type-eq-decl nil State 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)
    (assign const-decl "State" State nil))
   shostak))
(conditional_continuous 0
  (conditional_continuous-1 nil 3354078097
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (typepred "g!1")
        (("" (expand "scott_continuous?")
          ((""
            (case-replace
             "increasing?(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)))")
            (("1" (flatten)
              (("1" (expand "lub_preserving?")
                (("1" (skosimp)
                  (("1" (typepred "D!1")
                    (("1" (inst - "D!1")
                      (("1" (inst - "D!1")
                        (("1"
                          (lemma "lub_set_image" ("g" "f!1" "D" "D!1"))
                          (("1"
                            (lemma "lub_set_image"
                             ("g" "g!1" "D" "D!1"))
                            (("1" (assert)
                              (("1"
                                (typepred "lub(image(f!1, D!1))")
                                (("1"
                                  (typepred "lub(image(g!1, D!1))")
                                  (("1"
                                    (typepred
                                     "lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)), D!1))")
                                    (("1"
                                      (expand "least_upper_bound?")
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (replace -13)
                                          (("1"
                                            (replace -15)
                                            (("1"
                                              (inst
                                               -2
                                               "conditional(B(b!1), lub(image(f!1, D!1)), lub(image(g!1, D!1)))")
                                              (("1"
                                                (split -2)
                                                (("1"
                                                  (hide -2)
                                                  (("1"
                                                    (case
                                                     "(sq_le)(conditional(B(b!1), lub(image(f!1, D!1)),
                          lub(image(g!1, D!1))),lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)),
                        D!1)))")
                                                    (("1"
                                                      (typepred
                                                       "sq_le")
                                                      (("1"
                                                        (expand
                                                         "pointed_directed_complete_partial_order?")
                                                        (("1"
                                                          (expand
                                                           "directed_complete_partial_order?")
                                                          (("1"
                                                            (expand
                                                             "partial_order?")
                                                            (("1"
                                                              (flatten)
                                                              (("1"
                                                                (expand
                                                                 "antisymmetric?")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "conditional(B(b!1), lub(image(f!1, D!1)), lub(image(g!1, D!1)))"
                                                                   "lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)), D!1))")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide 2)
                                                      (("2"
                                                        (typepred
                                                         "lub(image(LAMBDA c: conditional(B(b!1),f!1(c),g!1(c)),D!1))")
                                                        (("2"
                                                          (name-replace
                                                           "LUB_C"
                                                           "lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)),
                        D!1))")
                                                          (("2"
                                                            (expand
                                                             "least_upper_bound?")
                                                            (("2"
                                                              (flatten)
                                                              (("2"
                                                                (expand
                                                                 "upper_bound?"
                                                                 -1)
                                                                (("2"
                                                                  (replace
                                                                   -14
                                                                   1
                                                                   rl)
                                                                  (("2"
                                                                    (replace
                                                                     -16
                                                                     1
                                                                     rl)
                                                                    (("2"
                                                                      (replace
                                                                       -16
                                                                       -7
                                                                       rl)
                                                                      (("2"
                                                                        (replace
                                                                         -14
                                                                         -5
                                                                         rl)
                                                                        (("2"
                                                                          (inst
                                                                           -5
                                                                           "conditional(B(b!1), g!1(lub(D!1)), LUB_C)")
                                                                          (("2"
                                                                            (split
                                                                             -5)
                                                                            (("1"
                                                                              (inst
                                                                               -7
                                                                               "conditional(B(b!1), LUB_C, f!1(lub(D!1)))")
                                                                              (("1"
                                                                                (split
                                                                                 -7)
                                                                                (("1"
                                                                                  (hide-all-but
                                                                                   (-1
                                                                                    -2
                                                                                    1))
                                                                                  (("1"
                                                                                    (expand
                                                                                     "sq_le")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "conditional")
                                                                                      (("1"
                                                                                        (skosimp*)
                                                                                        (("1"
                                                                                          (inst
                                                                                           -
                                                                                           "s1!1"
                                                                                           "s2!1")
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "s1!1"
                                                                                             "s2!1")
                                                                                            (("1"
                                                                                              (case-replace
                                                                                               "B(b!1)(s1!1)")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil)
                                                                                               ("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide
                                                                                   2)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "upper_bound?")
                                                                                    (("2"
                                                                                      (skosimp)
                                                                                      (("2"
                                                                                        (typepred
                                                                                         "r!1")
                                                                                        (("2"
                                                                                          (expand
                                                                                           "image"
                                                                                           -1)
                                                                                          (("2"
                                                                                            (skosimp)
                                                                                            (("2"
                                                                                              (replace
                                                                                               -1)
                                                                                              (("2"
                                                                                                (typepred
                                                                                                 "x!1")
                                                                                                (("2"
                                                                                                  (hide
                                                                                                   -2
                                                                                                   -3)
                                                                                                  (("2"
                                                                                                    (typepred
                                                                                                     "lub(D!1)")
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "least_upper_bound?")
                                                                                                      (("2"
                                                                                                        (flatten)
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "upper_bound?"
                                                                                                           -1)
                                                                                                          (("2"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "x!1")
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "increasing?")
                                                                                                              (("2"
                                                                                                                (inst
                                                                                                                 -14
                                                                                                                 "x!1"
                                                                                                                 "lub(D!1)")
                                                                                                                (("2"
                                                                                                                  (inst
                                                                                                                   -16
                                                                                                                   "x!1"
                                                                                                                   "lub(D!1)")
                                                                                                                  (("2"
                                                                                                                    (assert)
                                                                                                                    (("2"
                                                                                                                      (inst
                                                                                                                       -4
                                                                                                                       "conditional(B(b!1), f!1(x!1), g!1(x!1))")
                                                                                                                      (("1"
                                                                                                                        (expand
                                                                                                                         "sq_le")
                                                                                                                        (("1"
                                                                                                                          (skosimp)
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "conditional")
                                                                                                                            (("1"
                                                                                                                              (case-replace
                                                                                                                               "B(b!1)(s1!1)")
                                                                                                                              (("1"
                                                                                                                                (inst
                                                                                                                                 -6
                                                                                                                                 "s1!1"
                                                                                                                                 "s2!1")
                                                                                                                                (("1"
                                                                                                                                  (assert)
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil)
                                                                                                                               ("2"
                                                                                                                                (assert)
                                                                                                                                (("2"
                                                                                                                                  (inst
                                                                                                                                   -17
                                                                                                                                   "s1!1"
                                                                                                                                   "s2!1")
                                                                                                                                  (("2"
                                                                                                                                    (assert)
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil)
                                                                                                                       ("2"
                                                                                                                        (expand
                                                                                                                         "image")
                                                                                                                        (("2"
                                                                                                                          (inst
                                                                                                                           +
                                                                                                                           "x!1")
                                                                                                                          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"
                                                                              (hide
                                                                               2)
                                                                              (("2"
                                                                                (expand
                                                                                 "upper_bound?"
                                                                                 1)
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (typepred
                                                                                     "r!1")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "image"
                                                                                       -1)
                                                                                      (("2"
                                                                                        (skosimp)
                                                                                        (("2"
                                                                                          (typepred
                                                                                           "x!1")
                                                                                          (("2"
                                                                                            (replace
                                                                                             -2)
                                                                                            (("2"
                                                                                              (rewrite
                                                                                               "sq_le"
                                                                                               1)
                                                                                              (("2"
                                                                                                (skosimp)
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "conditional"
                                                                                                   1)
                                                                                                  (("2"
                                                                                                    (case-replace
                                                                                                     "B(b!1)(s1!1)")
                                                                                                    (("1"
                                                                                                      (typepred
                                                                                                       "lub(D!1)")
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "least_upper_bound?")
                                                                                                        (("1"
                                                                                                          (flatten)
                                                                                                          (("1"
                                                                                                            (expand
                                                                                                             "upper_bound?"
                                                                                                             -1)
                                                                                                            (("1"
                                                                                                              (inst
                                                                                                               -
                                                                                                               "x!1")
                                                                                                              (("1"
                                                                                                                (expand
                                                                                                                 "increasing?"
                                                                                                                 -18)
                                                                                                                (("1"
                                                                                                                  (inst
                                                                                                                   -18
                                                                                                                   "x!1"
                                                                                                                   "lub(D!1)")
                                                                                                                  (("1"
                                                                                                                    (assert)
                                                                                                                    (("1"
                                                                                                                      (expand
                                                                                                                       "sq_le"
                                                                                                                       -18)
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -18
                                                                                                                         "s1!1"
                                                                                                                         "s2!1")
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (assert)
                                                                                                      (("2"
                                                                                                        (inst
                                                                                                         -4
                                                                                                         "conditional(B(b!1), f!1(x!1), g!1(x!1))")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "sq_le"
                                                                                                           -4)
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "s1!1"
                                                                                                             "s2!1")
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "conditional"
                                                                                                               -4)
                                                                                                              (("1"
                                                                                                                (propax)
                                                                                                                nil
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (expand
                                                                                                           "image")
                                                                                                          (("2"
                                                                                                            (inst
                                                                                                             +
                                                                                                             "x!1")
                                                                                                            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))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide 2)
                                                  (("2"
                                                    (expand
                                                     "upper_bound?")
                                                    (("2"
                                                      (skosimp)
                                                      (("2"
                                                        (typepred
                                                         "r!1")
                                                        (("2"
                                                          (expand
                                                           "image"
                                                           -1)
                                                          (("2"
                                                            (skosimp)
                                                            (("2"
                                                              (typepred
                                                               "x!1")
                                                              (("2"
                                                                (replace
                                                                 -2)
                                                                (("2"
                                                                  (hide
                                                                   -2)
                                                                  (("2"
                                                                    (expand
                                                                     "sq_le"
                                                                     1)
                                                                    (("2"
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.76 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.