Quelle  lift_props.prf   Sprache: Lisp

(lift_props
 (down_up 0
  (down_up-1 nil 3353045582 ("" (grind) nil nil) nil shostak))
 (up_down 0
  (up_down-1 nil 3353049060
   ("" (skosimp) (("" (grind) (("" (decompose-equality) nil nil)) nil))
    nil)
   ((up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (lift_up_extensionality formula-decl nil lift_adt nil)
    (T formal-type-decl nil lift_props nil)
    (lift type-decl nil lift_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil))
   shostak))
 (down_equal 0
  (down_equal-1 nil 3353768866
   ("" (skosimp)
    (("" (case-replace "y1!1=y2!1")
      (("1" (assert) nil nil)
       ("2" (assert)
        (("2" (lemma "up_down" ("y" "y1!1"))
          (("2" (lemma "up_down" ("y" "y2!1")) (("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil lift_props nil)
    (lift type-decl nil lift_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (up_down formula-decl nil lift_props nil))
   shostak))
 (up_equal 0
  (up_equal-1 nil 3353045918
   ("" (skosimp)
    (("" (case-replace "x1!1=x2!1")
      (("1" (assert) nil nil)
       ("2" (assert)
        (("2" (lemma "down_equal" ("y1" "up(x1!1)" "y2" "up(x2!1)"))
          (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil lift_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (lift type-decl nil lift_adt nil)
    (down_equal formula-decl nil lift_props nil))
   shostak)))