[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Non empty finite set induction



Jerry,
I'm cc'ing the list to try and get our conversation back over
there. I've attached a dump of the original 'curry' theory, as well as
the 'dualton' theory you were working on, for background.

>I started working on these tonight, but only had time to prove the
>first two.  Maybe one of those will be enough to get you out of your
>current spot, though.  See the attached.  Also, "dualton" is a stupid
>name. :-)

The first two don't really help; I think the third one has potential
though. One that I'm working on is:

  sets_lemmas_ext[T: TYPE]: THEORY
  BEGIN
    a, b: VAR T
    A: VAR non_empty_finite_set[T]

    doubleton?(A): bool = singleton?(rest(A))

    remove_is_element: LEMMA
      FORALL (a, b: (A) | a /= b): doubleton?(A) IMPLIES
	remove(a, A) = singleton(b) AND remove(b, A) = singleton(a)
  END sets_lemmas_ext

Does this make sense? I get some dead-ends when trying to prove it, so
I may be missing something. Essentially, however, in the curry_x proof
it would be ideal to bring something like this in and instantiate it
with "k!1" and "choose(U!1)".

jerome
%% PVS Version 4.1 - CMU Common Lisp 19d (19D)
%% 19d (19D)
$$$curry.pvs
finite_sets_inductions_ext[T: TYPE]: THEORY
BEGIN
  IMPORTING finite_sets[T]

  SS,U : VAR non_empty_finite_set
  P : VAR pred[finite_set]
  n : VAR nat

  nonempty_finite_set_induction_gen: THEOREM
    (FORALL U:
      (FORALL SS: card(SS) < card(U) IMPLIES P(SS)) IMPLIES P(U))
        IMPLIES (FORALL U: P(U))

END finite_sets_inductions_ext

curry[R: TYPE, o: FUNCTION[R, R -> R]]: THEORY
BEGIN
  ASSUMING
    comm: ASSUMPTION commutative?(o)
    assc: ASSUMPTION associative?(o)
  ENDASSUMING

  index:   TYPE = posnat
  myset:   TYPE = ARRAY[index -> R]
  indices: TYPE = non_empty_finite_set[index]

  IMPORTING finite_sets@finite_sets_inductions[index]

  curry(s: myset, K: indices): RECURSIVE R =
    IF singleton?(K) THEN s(the(K))
    ELSE s(choose(K)) o curry(s, rest(K))
    ENDIF
  MEASURE card(K)

  IMPORTING finite_sets_inductions_ext[index]

  curry_singleton: LEMMA
    FORALL (s: myset, k: index): curry(s, singleton(k)) = s(k)

  curry_x: LEMMA
    FORALL (s: myset, K: indices, k: index):
      member(k, K) AND NOT singleton?(K) IMPLIES
        curry(s, K) = s(k) o curry(s, remove(k, K))

END curry

$$$curry.prf
(|finite_sets_inductions_ext|
 (|nonempty_finite_set_induction_gen| 0
  (|nonempty_finite_set_induction_gen-1| NIL 3420945053 NIL
   ("" (SKOSIMP)
    (("" (CASE "FORALL n, U: card(U) = n IMPLIES P!1(U)")
      (("1" (SKOLEM!) (("1" (INST -1 "card(U!1)" "U!1") NIL)))
       ("2" (HIDE 2)
        (("2" (INDUCT "n" + "NAT_induction")
          (("2" (SKOSIMP*)
            (("2" (INST -3 "U!1")
              (("2" (ASSERT)
                (("2" (SKOSIMP)
                  (("2" (INST -1 "card(SS!1)")
                    (("2" (ASSERT)
                      (("2" (INST -1 "SS!1") NIL))))))))))))))))))))
    NIL)
   PROVED
   ((|real_lt_is_strict_total_order| NAME-JUDGEMENT
     "(strict_total_order?[real])" |real_props| NIL)
    (|NAT_induction| FORMULA-DECL NIL |naturalnumbers| NIL)
    (|pred| TYPE-EQ-DECL NIL |defined_types| NIL)
    (|card| CONST-DECL "{n: nat | n = Card(S)}" |finite_sets| NIL)
    (|Card| CONST-DECL "nat" |finite_sets| NIL)
    (= CONST-DECL "[T, T -> boolean]" |equalities| NIL)
    (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL)
    (|non_empty_finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
    (|empty?| CONST-DECL "bool" |sets| NIL)
    (NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
    (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
    (|is_finite| CONST-DECL "bool" |finite_sets| NIL)
    (|set| TYPE-EQ-DECL NIL |sets| NIL)
    (T FORMAL-TYPE-DECL NIL |finite_sets_inductions_ext| NIL)
    (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL)
    (>= CONST-DECL "bool" |reals| NIL)
    (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| 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))
   NIL NIL NIL NIL)))
(|curry|
 (|curry_TCC1| 0
  (|curry_TCC1-1| NIL 3420944664 3420945128
   ("" (GRIND :EXCLUDE "choose") NIL NIL) PROVED
   ((|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
    (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
    (NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
    (|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL)
    (|number_field_pred| CONST-DECL "[number -> boolean]" |number_fields| NIL)
    (|number_field| NONEMPTY-TYPE-FROM-DECL NIL |number_fields| NIL)
    (|real_pred| CONST-DECL "[number_field -> boolean]" |reals| NIL)
    (|real| NONEMPTY-TYPE-FROM-DECL NIL |reals| NIL)
    (|rational_pred| CONST-DECL "[real -> boolean]" |rationals| NIL)
    (|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
    (|integer_pred| CONST-DECL "[rational -> boolean]" |integers| NIL)
    (|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
    (>= CONST-DECL "bool" |reals| NIL)
    (|nonneg_int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
    (> CONST-DECL "bool" |reals| NIL) (|index| TYPE-EQ-DECL NIL |curry| NIL)
    (|set| TYPE-EQ-DECL NIL |sets| NIL)
    (|is_finite| CONST-DECL "bool" |finite_sets| NIL)
    (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
    (|indices| TYPE-EQ-DECL NIL |curry| NIL)
    (|injective?| CONST-DECL "bool" |functions| NIL)
    (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL)
    (|real_ge_is_total_order| NAME-JUDGEMENT "(total_order?[real])"
     |real_props| NIL)
    (|real_gt_is_strict_total_order| NAME-JUDGEMENT
     "(strict_total_order?[real])" |real_props| NIL)
    (|choose| CONST-DECL "(p)" |sets| NIL)
    (|nonempty?| CONST-DECL "bool" |sets| NIL)
    (|finite_remove| APPLICATION-JUDGEMENT "finite_set[index]" |curry| NIL)
    (|singleton?| CONST-DECL "bool" |sets| NIL)
    (|rest| CONST-DECL "set" |sets| NIL)
    (/= CONST-DECL "boolean" |notequal| NIL)
    (|member| CONST-DECL "bool" |sets| NIL)
    (|remove| CONST-DECL "set" |sets| NIL)
    (|empty?| CONST-DECL "bool" |sets| NIL))
   832 126 T NIL))
 (|curry_TCC2| 0
  (|curry_TCC2-1| NIL 3420944664 3420945155
   ("" (SKOSIMP) (("" (REWRITE "card_rest") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   PROVED
   ((|int_minus_int_is_int| APPLICATION-JUDGEMENT "int" |integers| NIL)
    (|card_rest| FORMULA-DECL NIL |finite_sets| NIL)
    (|set| TYPE-EQ-DECL NIL |sets| NIL)
    (|is_finite| CONST-DECL "bool" |finite_sets| NIL)
    (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
    (NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
    (|empty?| CONST-DECL "bool" |sets| NIL)
    (|indices| TYPE-EQ-DECL NIL |curry| NIL)
    (|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL)
    (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
    (|number_field_pred| CONST-DECL "[number -> boolean]" |number_fields| NIL)
    (|number_field| NONEMPTY-TYPE-FROM-DECL NIL |number_fields| NIL)
    (|real_pred| CONST-DECL "[number_field -> boolean]" |reals| NIL)
    (|real| NONEMPTY-TYPE-FROM-DECL NIL |reals| NIL)
    (|rational_pred| CONST-DECL "[real -> boolean]" |rationals| NIL)
    (|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
    (|integer_pred| CONST-DECL "[rational -> boolean]" |integers| NIL)
    (|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
    (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
    (>= CONST-DECL "bool" |reals| NIL)
    (|nonneg_int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
    (> CONST-DECL "bool" |reals| NIL) (|index| TYPE-EQ-DECL NIL |curry| NIL)
    (|real_lt_is_strict_total_order| NAME-JUDGEMENT
     "(strict_total_order?[real])" |real_props| NIL))
   758 28 T NIL))
 (|curry_singleton| 0
  (|curry_singleton-1| NIL 3420945323 3420945381
   ("" (SKOLEM!)
    (("" (TYPEPRED "the(singleton(k!1))")
      (("" (EXPAND "curry")
        (("" (REWRITE "singleton")
          (("" (REWRITE "the") (("" (ASSERT) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   PROVED
   ((|nonempty_singleton_finite| APPLICATION-JUDGEMENT
     "non_empty_finite_set[index]" |curry| NIL)
    (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
    (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
    (NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
    (|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL)
    (|number_field_pred| CONST-DECL "[number -> boolean]" |number_fields| NIL)
    (|number_field| NONEMPTY-TYPE-FROM-DECL NIL |number_fields| NIL)
    (|real_pred| CONST-DECL "[number_field -> boolean]" |reals| NIL)
    (|real| NONEMPTY-TYPE-FROM-DECL NIL |reals| NIL)
    (> CONST-DECL "bool" |reals| NIL)
    (|rational_pred| CONST-DECL "[real -> boolean]" |rationals| NIL)
    (|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
    (|integer_pred| CONST-DECL "[rational -> boolean]" |integers| NIL)
    (|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
    (>= CONST-DECL "bool" |reals| NIL)
    (|nonneg_int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
    (|index| TYPE-EQ-DECL NIL |curry| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL)
    (|singleton?| CONST-DECL "bool" |sets| NIL)
    (|the| CONST-DECL "(p)" |sets| NIL)
    (|singleton| CONST-DECL "(singleton?)" |sets| NIL)
    (|real_gt_is_strict_total_order| NAME-JUDGEMENT
     "(strict_total_order?[real])" |real_props| NIL)
    (|curry| DEF-DECL "R" |curry| NIL))
   5718 10 T SHOSTAK))
 (|curry_x_TCC1| 0
  (|curry_x_TCC1-1| NIL 3420944664 3420945312 ("" (SUBTYPE-TCC) NIL NIL) PROVED
   ((|empty?| CONST-DECL "bool" |sets| NIL)
    (|remove| CONST-DECL "set" |sets| NIL)
    (/= CONST-DECL "boolean" |notequal| NIL)
    (|singleton?| CONST-DECL "bool" |sets| NIL)
    (|member| CONST-DECL "bool" |sets| NIL)
    (|finite_remove| APPLICATION-JUDGEMENT "finite_set[index]" |curry| NIL)
    (|real_ge_is_total_order| NAME-JUDGEMENT "(total_order?[real])"
     |real_props| NIL)
    (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL)
    (|real_gt_is_strict_total_order| NAME-JUDGEMENT
     "(strict_total_order?[real])" |real_props| NIL)
    (|injective?| CONST-DECL "bool" |functions| NIL)
    (|indices| TYPE-EQ-DECL NIL |curry| NIL)
    (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL)
    (|is_finite| CONST-DECL "bool" |finite_sets| NIL)
    (|set| TYPE-EQ-DECL NIL |sets| NIL) (|index| TYPE-EQ-DECL NIL |curry| NIL)
    (> CONST-DECL "bool" |reals| NIL)
    (|nonneg_int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
    (>= CONST-DECL "bool" |reals| 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)
    (NOT CONST-DECL "[bool -> bool]" |booleans| NIL)
    (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
    (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL))
   158 158 T NIL))
 (|curry_x| 0
  (|curry_x-2| NIL 3420945537 3420945585
   ("" (INDUCT "K" :NAME "nonempty_finite_set_induction_gen")
    (("1" (TYPEPRED "K!1") (("1" (PROPAX) NIL NIL)) NIL)
     ("2" (SKOSIMP*)
      (("2" (EXPAND "curry" 3 1)
        (("2" (SMASH)
          (("2" (COPY -1)
            (("2" (INST -2 "rest(U!1)")
              (("2" (INST -1 "remove(k!1, U!1)")
                (("2" (REWRITE "card_rest")
                  (("2" (REWRITE "card_remove")
                    (("2" (REWRITE "member")
                      (("2" (ASSERT)
                        (("2" (INST -1 "s!1" "choose(U!1)")
                          (("2" (INST -2 "s!1" "k!1")
                            (("2" (GROUND)
                              (("1"
                                (CASE-REPLACE
                                 "remove(choose(U!1), remove(k!1, U!1)) = remove(k!1, rest(U!1))")
                                (("1" (REPLACE -3)
                                  (("1" (REPLACE -2)
                                    (("1" (LEMMA "assc")
                                      (("1" (EXPAND "associative?")
                                        (("1" (COPY -1)
                                          (("1"
                                            (INST -1 "s!1(choose(U!1))"
                                             "s!1(k!1)"
                                             "curry(s!1, remove(k!1, rest(U!1)))")
                                            (("1"
                                              (INST -2 "s!1(k!1)"
                                               "s!1(choose(U!1))"
                                               "curry(s!1, remove(k!1, rest(U!1)))")
                                              (("1" (REPLACE -1 :DIR RL)
                                                (("1" (REPLACE -2 :DIR RL)
                                                  (("1" (LEMMA "comm")
                                                    (("1"
                                                      (EXPAND "commutative?")
                                                      (("1"
                                                        (INST -1
                                                         "s!1(choose(U!1))"
                                                         "s!1(k!1)")
                                                        (("1" (REPLACE -1)
                                                          (("1" (PROPAX) NIL
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("2" (HIDE-ALL-BUT 1)
                                  (("2" (GRIND-WITH-EXT :EXCLUDE "choose") NIL
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (GRIND :EXCLUDE "curry") NIL NIL)
                               ("3" (HIDE -2)
                                (("3" (REWRITE "rest")
                                  (("3" (POSTPONE) NIL NIL)) NIL))
                                NIL)
                               ("4" (GRIND :EXCLUDE "choose") NIL NIL)
                               ("5" (GRIND :EXCLUDE "curry") NIL NIL)
                               ("6" (GRIND :EXCLUDE "choose") NIL NIL)
                               ("7" (HIDE -1)
                                (("7" (REWRITE "rest")
                                  (("7" (POSTPONE) NIL NIL)) NIL))
                                NIL)
                               ("8" (GRIND :EXCLUDE "curry") NIL NIL)
                               ("9" (REWRITE "rest") (("9" (POSTPONE) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("3" (SKOSIMP*) (("3" (GRIND :EXCLUDE "curry") NIL NIL)) NIL))
    NIL)
   UNFINISHED NIL 4703 397 NIL NIL)))

%% PVS Version 4.1 - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Oct 30, 2007 14:52)
%% 8.1 [Linux (x86)] (Oct 30, 2007 14:52)
$$$dualton.pvs
%-------------------------------------------------------------------------
%
%  Sets with exactly two elements
%
%  For PVS version 4.1.  May 28, 2008
%  ---------------------------------------------------------------------
%      Author: Jerry James <loganjerry@xxxxxxxxx>
%
%-------------------------------------------------------------------------
dualton[T: TYPE]: THEORY
 BEGIN

  IMPORTING sets[T]

  t, u, v: VAR T
  S: VAR set

  % A set with exactly two elements
  dualton?(S): bool = EXISTS t, u: t /= u AND S = ({v | v = t OR v = u})

  dualton(t: T, u: {v | t /= v}): (dualton?) = {v | v = t OR v = u}

  D: VAR (dualton?)

  dualton_nonempty: JUDGEMENT (dualton?) SUBTYPE_OF (nonempty?)

  dualton_remove: LEMMA
    FORALL t, D: member(t, D) IMPLIES singleton?(remove(t, D))

  dualton_rest: LEMMA FORALL D: singleton?(rest(D))

  dualton_choose: LEMMA
    FORALL t, u:
      t /= u IMPLIES
       (choose(dualton(t, u)) = t AND rest(dualton(t, u)) = singleton(u))
        OR
        (choose(dualton(t, u)) = u AND rest(dualton(t, u)) = singleton(t))

 END dualton

$$$dualton.prf
(dualton
 (dualton_TCC1 0
  (dualton_TCC1-1 nil 3421022779 3421023157 ("" (subtype-tcc) nil nil)
   proved
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil dualton nil)
    (/= const-decl "boolean" notequal nil)
    (dualton? const-decl "bool" dualton nil))
   66 40 nil nil))
 (dualton_nonempty 0
  (dualton_nonempty-1 nil 3421023156 3421023157
   ("" (judgement-tcc) nil nil) proved
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (dualton? const-decl "bool" dualton nil)
    (/= const-decl "boolean" notequal nil)
    (T formal-type-decl nil dualton nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil))
   117 80 nil nil))
 (dualton_remove 0
  (dualton_remove-1 nil 3421022787 3421023157
   ("" (grind :if-match nil)
    (("1" (inst + "u!1")
      (("1" (grind-with-ext) nil nil) ("2" (grind-with-ext) nil nil))
      nil)
     ("2" (inst + "t!2")
      (("1" (grind-with-ext) nil nil) ("2" (grind-with-ext) nil nil))
      nil))
    nil)
   proved
   ((t!2 skolem-const-decl "T" dualton nil)
    (D!1 skolem-const-decl "(dualton?)" dualton nil)
    (u!1 skolem-const-decl "T" dualton nil)
    (remove const-decl "set" sets nil)
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (dualton? const-decl "bool" dualton nil)
    (singleton? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (T formal-type-decl nil dualton nil))
   337 260 t shostak))
 (dualton_rest 0
  (dualton_rest-1 nil 3421022975 3421023688
   ("" (skolem-typepred)
    (("" (expand "rest")
      (("" (ground)
        (("1" (use "dualton_nonempty")
          (("1" (expand "nonempty?") (("1" (propax) nil nil)) nil))
          nil)
         ("2" (use "dualton_remove")
          (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   proved
   ((rest const-decl "set" sets nil)
    (dualton_remove formula-decl nil dualton nil)
    (choose const-decl "(p)" sets nil)
    (member const-decl "bool" sets nil)
    (dualton_nonempty judgement-tcc nil dualton nil)
    (nonempty? const-decl "bool" sets nil)
    (dualton? const-decl "bool" dualton nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil dualton nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   69345 100 t shostak))
 (dualton_choose 0
  (dualton_choose-1 nil 3421023602 3421023733
   ("" (skosimp) (("" (postpone) nil nil)) nil) unfinished nil 12238 10
   t shostak)))