Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 693


Synopsis:        Error when saving proofs
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Jul 30 16:35:01 2002
Originator:      Bruno Dutertre
Organization:    sdl.sri.com
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------050201060006020300050005
  Content-Type: text/plain; charset=us-ascii; format=flowed
  Content-Transfer-Encoding: 7bit
  
  Sam,
  
  In the attached dump, PVS3.0 broke when I modified an
  existing proof (sum_update). When saving it, I got:
  
  Would you like the proof to be saved? (Yes or No) yes
  Would you like to overwrite the current proof (named sum_update-1)? (Yes 
  or No) yes
  
  Run time  = 10.71 secs.
  Real time = 344.30 secs.
  
  
  Run time  = 11.09 secs.
  Real time = 344.30 secs.
  Error: No methods applicable for generic function
          #<standard-generic-function library> with args
          (#<Library-theory finite_sets>) of classes (library-theory)
     [condition type: program-error]
  
  Restart actions (select using :continue):
    0: Try calling it again
    1: Return to Top Level (an "abort" restart)
    2: Abort #<process Initial Lisp Listener>
  [1c] pvs(100):
  
  
  
  
  Bruno
  
  --------------050201060006020300050005
  Content-Type: text/plain;
   name="fset_sums.dmp"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="fset_sums.dmp"
  
  
  $$$fsets_sum.pvs
  %------------------------------------------------------------------------
  %  Finite sum over real-valued functions
  %  (reworked from Ricky Butler's version in finite set lib)
  %------------------------------------------------------------------------
  
  fsets_sum[T: TYPE]: THEORY
  
    BEGIN
  
  %%  IMPORTING finite_sets@finite_sets_sum[T,real,0,+]
  
    IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_inductions
  
    S, A, B: VAR finite_set[T]
    E: VAR non_empty_finite_set[T]
    t, x, x1, x2: VAR T
    c, N: VAR real
    f, g: VAR function[T -> real]
  
  
  
  %% Things below and up to sum_distributive have been
  %% copied from finite_set@finite_sets_sum.
  %%
  %% Shouldn't need to do that but there was a problem with
  %% judgements otherwise. Bug in PVS: I can't reverse the 
  %% change? (7/19/99)
  %%
  %% Fixed by Sam (9/1/99) but still things do not work so well
  %% (auto-rewrite in proof of sum_indexed_partitions.sum_partition)
  %%
  
    %------------------------------------
    %  Definition and basic properties
    %------------------------------------
  
    sum(S, f) : RECURSIVE real  = 
        IF (empty?(S)) THEN 0 ELSE f(choose(S)) + sum(rest(S),f) ENDIF 
     MEASURE card(S)
  
  
    sum_emptyset  : THEOREM sum(emptyset, f) = 0
  
    sum_singleton : THEOREM sum(singleton(x), f) = f(x)
  
    sum_x         : THEOREM FORALL (x: (S)): sum(S, f) = f(x) + sum(remove(x, S
 ), f)
  
    sum_x1_x2     : THEOREM FORALL (x1, x2: (S)): 
  				f(x1) + sum(remove(x1, S), f) = f(x2) + sum(rem
 ove(x2, S), f)
  
    sum_add       : THEOREM sum(add(x, S),f) = 
  				IF S(x) THEN sum(S, f) ELSE sum(S, f) + f(x) EN
 DIF
  
    sum_remove    : THEOREM sum(remove(x, S),f) = 
  				IF S(x) THEN sum(S, f) - f(x) ELSE sum(S, f) EN
 DIF
  
    sum_rest      : THEOREM NOT empty?(S) IMPLIES 
  				f(choose(S)) + sum(rest(S),f) = sum(S,f)
   
    sum_disj_union: THEOREM disjoint?(A, B) IMPLIES 
  				sum(union(A, B), f) = sum(A, f) + sum(B, f) 
  
    sum_diff_subset: THEOREM subset?(A, B) IMPLIES 
  				sum(difference(B, A), f) = sum(B, f) - sum(A, f
 )
  
    sum_union      : THEOREM sum(union(A, B), f) + sum(intersection(A, B),f ) =
  sum(A, f) + sum(B, f) 
  
    sum_diff_intersection: THEOREM sum(A, f) = sum(difference(A, B), f) + sum(i
 ntersection(A, B), f) 
  
    sum_f_g         : THEOREM (FORALL (x: (S)): f(x) = g(x)) IMPLIES sum(S, f) 
 = sum(S, g)
  
    sum_particular  : THEOREM sum(S, f WITH [x := c]) = 
  				IF S(x) THEN  sum(S, f) + c - f(x) ELSE sum(S, 
 f) ENDIF 
  
    sum_distributive: THEOREM sum(A, f) + sum(A, g) = sum(A, LAMBDA x: f(x) + g
 (x)) 
  
  
  
    %---------------------------
    %  Sum for a few functions
    %---------------------------
  
    sum_const    : THEOREM sum(S, (LAMBDA t: c)) = c*card(S) 
  
    sum_mult     : THEOREM sum(S,(LAMBDA t: c*f(t))) = c*sum(S,f) 
  
    sum_1_is_card: THEOREM sum(S,(LAMBDA t: 1)) = card(S)
  
    sum_update   : THEOREM sum(S, f WITH [(t) := c]) =
  			     IF S(t) THEN sum(S, f) - f(t) + c ELSE sum(S, f) E
 NDIF
  
  
    %------------------------------------------------------
    %  Ordering properties for two sums over the same set
    %------------------------------------------------------
  
    sum_le       : THEOREM (FORALL (t: (S)): f(t) <= g(t))
                               IMPLIES sum(S, f) <= sum(S, g)
  
    sum_ge       : THEOREM (FORALL (t: (S)): f(t) >= g(t))
                               IMPLIES sum(S, f) >= sum(S, g)
  
    sum_lt       : THEOREM (FORALL (t: (E)): f(t) < g(t))
                               IMPLIES sum(E, f) < sum(E, g)
  
    sum_gt       : THEOREM (FORALL (t: (E)): f(t) > g(t))
                               IMPLIES sum(E, f) > sum(E, g)
  
  
    %------------------------------------------------
    %  Bounds on sum derived from bounds of f on S
    %------------------------------------------------
  
    sum_bound    : THEOREM (FORALL (t: (S)): f(t) <= N) 
                               IMPLIES sum(S,f) <= N*card(S)
  
    sum_bound2   : THEOREM (FORALL (t: (S)): f(t) >= N) 
                               IMPLIES sum(S,f) >= N*card(S)
  
    sum_bound3   : THEOREM (FORALL (t: (E)): f(t) < N) 
                               IMPLIES sum(E,f) < N*card(E)
  
    sum_bound4   : THEOREM (FORALL (t: (E)): f(t) > N) 
                               IMPLIES sum(E,f) > N*card(E)
  
  
    %---------------------
    %  Sign of sum(S, f)
    %---------------------
  
    sum_nonneg   : LEMMA (FORALL (t: (S)): f(t) >= 0) IMPLIES sum(S,f) >= 0
  
    sum_nonpos   : LEMMA (FORALL (t: (S)): f(t) <= 0) IMPLIES sum(S,f) <= 0
  
    sum_pos      : LEMMA (FORALL (t: (S)): f(t) >= 0) 
  			   AND (EXISTS (t: (S)): f(t) > 0) IMPLIES sum(S, f) > 
 0
  
    sum_pos2     : LEMMA (FORALL (t: (E)): f(t) > 0) IMPLIES sum(E,f) > 0
  
    sum_neg      : LEMMA (FORALL (t: (S)): f(t) <= 0) 
  			   AND (EXISTS (t: (S)): f(t) < 0) IMPLIES sum(S, f) < 
 0
  
    sum_neg2     : LEMMA (FORALL (t: (E)): f(t) < 0) IMPLIES sum(E,f) < 0
  
    sum_zero     : LEMMA (FORALL (t: (S)): f(t) = 0) IMPLIES sum(S, f) = 0
  
  
  
    %-----------------------
    %  Closure properties
    %-----------------------
  
    U: VAR set[real]  
  
    sum_closure1: LEMMA 
       (FORALL (a, b: (U)): U(a+b)) AND (FORALL (t: (E)): U(f(t))) 
  	  IMPLIES U(sum(E, f))
  
    sum_closure2: LEMMA 
       U(0) AND (FORALL (a, b: (U)): U(a+b)) AND (FORALL (t: (S)): U(f(t))) 
  	  IMPLIES U(sum(S, f))
  
  
    %---------------
    %   Judgements
    %---------------
  
    nnf: VAR [T -> nonneg_real]
    npf: VAR [T -> nonpos_real]
    pf:  VAR [T -> posreal]
    nf:  VAR [T -> negreal]
  
    sum_nnreal_is_nnreal:   JUDGEMENT sum(S, nnf) HAS_TYPE nonneg_real
    sum_npreal_is_npreal:   JUDGEMENT sum(S, npf) HAS_TYPE nonpos_real
    sum_posreal_is_posreal: JUDGEMENT sum(E, pf)  HAS_TYPE posreal
    sum_negreal_is_negreal: JUDGEMENT sum(E, nf)  HAS_TYPE negreal
  
  
    u:   VAR [T -> rat]
    nnu: VAR [T -> nonneg_rat]
    npu: VAR [T -> nonpos_rat]
    pu:  VAR [T -> posrat]
    nu:  VAR [T -> negrat]
  
    sum_rat_is_rat:       JUDGEMENT sum(S, u)   HAS_TYPE rat
    sum_nnrat_is_nnrat:   JUDGEMENT sum(S, nnu) HAS_TYPE nonneg_rat
    sum_nprat_is_nprat:   JUDGEMENT sum(S, npu) HAS_TYPE nonpos_rat
    sum_posrat_is_posrat: JUDGEMENT sum(E, pu)  HAS_TYPE posrat
    sum_negrat_is_negrat: JUDGEMENT sum(E, nu)  HAS_TYPE negrat
  
  
    v:   VAR [T -> int]
    npv: VAR [T -> nonpos_int]
    nv:  VAR [T -> negint]
  
    sum_int_is_int:       JUDGEMENT sum(S, v)   HAS_TYPE int
    sum_npint_is_npint:   JUDGEMENT sum(S, npv) HAS_TYPE nonpos_int
    sum_negint_is_negint: JUDGEMENT sum(E, nv)  HAS_TYPE negint
  
    w:   VAR [T -> nat]
    pw:  VAR [T -> posnat]
  
    sum_nat_is_nat:       JUDGEMENT sum(S, w)  HAS_TYPE nat
    sum_posnat_is_posnat: JUDGEMENT sum(E, pw) HAS_TYPE posnat
  
  
  
    %-------------------------------------------------------
    %  Properties of f derived from the value of Sum(S, f) 
    %-------------------------------------------------------
  
    sum_max_bound  : THEOREM sum(S,f) = N * card(S) AND (FORALL (t: (S)): f(t) 
 <= N)
  			      IMPLIES (FORALL (t: (S)): f(t) = N)
  
    sum_min_bound  : THEOREM sum(S,f) = N * card(S) AND (FORALL (t: (S)): f(t) 
 >= N)
  			      IMPLIES (FORALL (t: (S)): f(t) = N)
  
    sum_0_non_neg  : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) >= 0) 
                               IMPLIES (FORALL (t: (S)): f(t) = 0)
    
    sum_0_non_pos  : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) <= 0) 
                               IMPLIES (FORALL (t: (S)): f(t) = 0)
  
    equal_sum_le   : THEOREM sum(S, f) = sum(S, g) AND (FORALL (t: (S)): f(t) <
 = g(t))
  			     IMPLIES (FORALL (t: (S)): f(t) = g(t))
  
    equal_sum_ge   : THEOREM sum(S, f) = sum(S, g) AND (FORALL (t: (S)): f(t) >
 = g(t))
  			     IMPLIES (FORALL (t: (S)): f(t) = g(t))
  
    h, h1, h2: VAR function[T -> nonneg_real]
  
    sum_0_non_neg2 : COROLLARY sum(S, h) = 0 IMPLIES (FORALL (t : (S)) : h(t) =
  0)
  
  
    k, k1, k2: VAR function[T -> nonpos_real]
  
    sum_0_non_pos2 : COROLLARY sum(S, k) = 0 IMPLIES (FORALL (t : (S)) : k(t) =
  0)
  
  
  
    %--------------------------------------------------
    %  Some relations between Sum(A, f) AND Sum(B, f)
    %   when A is a subset of B
    %--------------------------------------------------
  
    sum_subset: THEOREM subset?(A, B) IMPLIES sum(A, h) <= sum(B, h)
  
    sum_subset2: THEOREM subset?(A, B) IMPLIES sum(A, k) >= sum(B, k)
  
  
    sum_order_sub: THEOREM subset?(A, B) AND (FORALL (t:T): h1(t) <= h2(t))
          IMPLIES sum(A, h1) <= sum(B, h2)
  
    sum_order_sub2: THEOREM subset?(A, B) AND (FORALL (t:T): k1(t) >= k2(t))
          IMPLIES sum(A, k1) >= sum(B, k2)
  
  
    sum_subset3: THEOREM
       subset?(A, B) AND (FORALL (t: (B)): A(t) OR f(t) = 0)
  	IMPLIES sum(A, f) = sum(B, f)
  
    END fsets_sum
  
  
  $$$fsets_sum.prf
  (|fsets_sum| (|sum_TCC1| "" (GRIND) NIL NIL)
   (|sum_TCC2| "" (AUTO-REWRITE "nonempty?" "card_rest")
    (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_TCC3| "" (TERMINATION-TCC)) (|sum_emptyset| "" (GRIND) NIL NIL)
   (|sum_singleton_TCC1| "" (SUBTYPE-TCC))
   (|sum_singleton| ""
    (AUTO-REWRITE "singleton" "sum_emptyset" "nonempty?")
    (("" (SKOLEM!)
      (("" (EXPAND "sum")
        (("" (CASE "empty?(singleton(x!1))")
          (("1" (DELETE +) (("1" (GRIND) NIL NIL)) NIL)
           ("2" (ASSERT)
            (("2" (TYPEPRED "choose(singleton(x!1))")
              (("2" (CASE-REPLACE "rest(singleton(x!1)) = emptyset")
                (("1" (REDUCE) NIL NIL)
                 ("2" (DELETE 3)
                  (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("2" (GRIND :EXCLUDE ("empty?" "choose")) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_x_TCC1| "" (SUBTYPE-TCC))
   (|sum_x| "" (SKOLEM + (_ "f!1" _))
    ((""
      (AUTO-REWRITE "sum" "nonempty?" "emptyset" "card_rest"
                    "card_remove")
      (("" (INDUCT "S" :NAME "finite_set_induction_gen[T]")
        (("" (SKOSIMP)
          (("" (SKOLEM-TYPEPRED)
            (("" (CASE "empty?(S!1)")
              (("1" (DELETE -3 1) (("1" (GRIND) NIL NIL)) NIL)
               ("2" (ASSERT)
                (("2" (CASE "rest(S!1)(x!1)")
                  (("1" (INST-CP - "rest(S!1)")
                    (("1" (INST - "remove(x!1, S!1)")
                      (("1" (ASSERT)
                        (("1" (INST - "choose(S!1)")
                          (("1" (INST - "x!1")
                            (("1"
                              (CASE-REPLACE
                               "remove(x!1, rest(S!1)) = remove(choose(S!1), re
 move(x!1, S!1))")
                              (("1" (ASSERT) NIL NIL)
                               ("2" (DELETE -3 -4 2 3)
                                (("2"
                                  (AUTO-REWRITE "remove" "rest" "member")
                                  (("2"
                                    (APPLY-EXTENSIONALITY :HIDE? T)
                                    (("2" (SMASH) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (DELETE -3 2 3)
                            (("2" (AUTO-REWRITE "remove" "rest" "member")
                              (("2" (REDUCE) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (DELETE -2)
                    (("2" (AUTO-REWRITE "rest" "member" "remove")
                      (("2" (REDUCE) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_x1_x2_TCC1| "" (SUBTYPE-TCC))
   (|sum_x1_x2| "" (SKOLEM!)
    (("" (REWRITE "sum_x" :DIR RL)
      (("" (REWRITE "sum_x" :DIR RL) NIL NIL)) NIL))
    NIL)
   (|sum_add_TCC1| "" (SUBTYPE-TCC))
   (|sum_add| "" (SKOLEM!)
    (("" (SMASH)
      (("1" (CASE-REPLACE "add(x!1, S!1) = S!1")
        (("1" (DELETE 2)
          (("1" (AUTO-REWRITE "add" "member")
            (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (SMASH) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (AUTO-REWRITE "add")
        (("2" (USE "sum_x" ("S" "add(x!1, S!1)"))
          (("2" (CASE-REPLACE "remove(x!1, add(x!1, S!1)) = S!1")
            (("2" (DELETE -1 3)
              (("2" (AUTO-REWRITE "remove" "add" "member")
                (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                  (("2" (SMASH) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_remove_TCC1| "" (SUBTYPE-TCC))
   (|sum_remove| "" (SKOLEM!)
    (("" (SMASH)
      (("1" (USE "sum_x") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (CASE-REPLACE "remove(x!1, S!1) = S!1")
        (("2" (DELETE 3)
          (("2" (AUTO-REWRITE-DEFS)
            (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_rest| "" (AUTO-REWRITE "sum") (("" (REDUCE) NIL NIL)) NIL)
   (|sum_disj_union_TCC1| "" (SUBTYPE-TCC))
   (|sum_disj_union| ""
    (AUTO-REWRITE "sum_add" "sum_emptyset" "union" "member" "disjoint?"
                  "intersection" "add" "empty?" "emptyset")
    (("" (SKOLEM + ("A!1" _ "f!1"))
      (("" (INDUCT "B" :NAME "finite_set_ind_modified[T]")
        (("1" (GROUND)
          (("1" (CASE-REPLACE "union(A!1, emptyset[T]) = A!1")
            (("1" (DELETE -1 2)
              (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (SKOSIMP)
          (("2" (GROUND)
            (("1" (INST - "e!1")
              (("1"
                (CASE-REPLACE
                 "union(A!1, add(e!1, S!1)) = add(e!1, union(A!1, S!1))")
                (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)
                 ("2" (DELETE -1 3 4)
                  (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("2" (SMASH) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_diff_subset_TCC1| "" (SUBTYPE-TCC))
   (|sum_diff_subset| "" (SKOSIMP)
    (("" (USE "sum_disj_union" ("A" "A!1" "B" "difference(B!1, A!1)"))
      (("" (GROUND)
        (("1" (CASE-REPLACE "union(A!1, difference(B!1, A!1)) = B!1")
          (("1" (ASSERT) NIL NIL)
           ("2" (DELETE -1 2)
            (("2" (AUTO-REWRITE-DEFS)
              (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                (("2" (REDUCE) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL)
         ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_union_TCC1| "" (SUBTYPE-TCC))
   (|sum_union_TCC2| "" (SUBTYPE-TCC))
   (|sum_union| "" (SKOLEM!)
    (("" (USE "sum_diff_subset" ("A" "A!1" "B" "union(A!1, B!1)"))
      (("" (GROUND)
        (("1"
          (USE "sum_diff_subset"
               ("A" "intersection(A!1, B!1)" "B" "B!1"))
          (("1" (GROUND)
            (("1"
              (CASE-REPLACE
               "difference(union(A!1, B!1), A!1) = difference(B!1, intersection
 (A!1, B!1))")
              (("1" (ASSERT) NIL NIL)
               ("2" (DELETE -1 -2 2)
                (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                  (("2" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_diff_intersection_TCC1| "" (SUBTYPE-TCC))
   (|sum_diff_intersection| "" (SKOLEM!)
    (("" (REWRITE "sum_disj_union" :DIR RL)
      (("1"
        (CASE-REPLACE
         "union(difference(A!1, B!1), intersection(A!1, B!1)) = A!1")
        (("1" (DELETE 2)
          (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL))
            NIL))
          NIL))
        NIL)
       ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL)
   (|sum_f_g| "" (SKOLEM + (_ "f!1" "g!1"))
    (("" (AUTO-REWRITE "sum" "sum_emptyset" "nonempty?")
      (("" (INDUCT "S" :NAME "finite_set_induction_rest[T]")
        (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (SKOSIMP)
          (("2" (GROUND)
            (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
             ("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("choose")) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_particular| "" (SKOLEM!)
    (("" (SMASH)
      (("1" (USE "sum_remove" ("f" "f!1"))
        (("1" (USE "sum_remove" ("f" "f!1 WITH [x!1 := c!1]"))
          (("1" (ASSERT)
            (("1" (USE "sum_f_g" ("g" "f!1"))
              (("1" (GROUND)
                (("1" (DELETE -1 -2 2) (("1" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (REWRITE "sum_f_g") NIL NIL))
      NIL))
    NIL)
   (|sum_distributive| "" (SKOLEM + (_ "f!1" "g!1"))
    (("" (AUTO-REWRITE "sum" "sum_emptyset" "nonempty?")
      (("" (INDUCT "A" :NAME "finite_set_induction_rest[T]")
        (("1" (ASSERT) NIL NIL)
         ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_const| ""
    (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
     NIL :REWRITES ("sum" "sum_emptyset" "card_emptyset" "card_rest"))
    NIL NIL)
   (|sum_mult| ""
    (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
     NIL :REWRITES ("sum" "sum_emptyset"))
    NIL NIL)
   (|sum_1_is_card| "" (SKOLEM!)
    (("" (REWRITE "sum_const") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_update| "" (SKOLEM!)
    (("" (SMASH)
      (("1" (AUTO-REWRITE "member")
        (("1" (USE "sum_remove")
          (("1" (USE "sum_remove" ("f" "f!1 WITH [(t!1) := c!1]"))
            (("1" (ASSERT)
              (("1"
                (CASE "sum(remove(t!1, S!1), f!1) = sum(remove(t!1, S!1), f!1 W
 ITH [(t!1) := c!1])")
                (("1" (ASSERT) NIL NIL)
                 ("2" (REWRITE "sum_f_g")
                  (("2" (DELETE -1 -2 2 3) (("2" (GRIND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (REWRITE "sum_f_g") NIL NIL))
      NIL))
    NIL)
   (|sum_le| ""
    (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
     NIL :REWRITES ("sum" "sum_emptyset" "nonempty?") :IF-MATCH NIL)
    (("" (INST - "f!1" "g!1")
      (("" (GROUND)
        (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (DELETE 2)
          (("2" (AUTO-REWRITE "rest" "remove" "member")
            (("2" (REDUCE) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_ge| "" (SKOSIMP)
    (("" (USE "sum_le" ("f" "g!1" "g" "f!1")) (("" (REDUCE) NIL NIL))
      NIL))
    NIL)
   (|sum_lt| ""
    (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :DEFS
     NIL :REWRITES ("sum_singleton" "sum_add") :THEORIES ("sets[T]")
     :IF-MATCH NIL)
    (("1" (INST?) NIL NIL)
     ("2" (INST - "f!1" "g!1")
      (("2" (GROUND)
        (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (DELETE 2 3) (("2" (REDUCE) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_gt| "" (SKOSIMP)
    (("" (USE "sum_lt" ("f" "g!1" "g" "f!1")) (("" (REDUCE) NIL NIL))
      NIL))
    NIL)
   (|sum_bound| "" (SKOLEM + ("N!1" _ "f!1"))
    ((""
      (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
       NIL :REWRITES
       ("sum" "card_emptyset" "card_rest" "sum_emptyset" "nonempty?"))
      (("" (TYPEPRED "t!1")
        (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_bound2| "" (SKOLEM + ("N!1" _ "f!1"))
    ((""
      (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
       NIL :REWRITES
       ("sum" "card_emptyset" "card_rest" "sum_emptyset" "nonempty?"))
      (("" (TYPEPRED "t!1")
        (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_bound3| ""
    (AUTO-REWRITE "sum_singleton" "card_singleton" "sum_add" "card_add")
    (("" (AUTO-REWRITE-THEORY "sets[T]")
      ((""
        (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]"
         :DEFS NIL)
        NIL NIL))
      NIL))
    NIL)
   (|sum_bound4| ""
    (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :DEFS
     NIL :REWRITES
     ("sum_singleton" "card_singleton" "sum_add" "card_add") :THEORIES
     "sets[T]")
    NIL NIL)
   (|sum_nonneg| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "sum_bound2") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_nonpos| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "sum_bound") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_pos| "" (SKOSIMP*)
    (("" (AUTO-REWRITE "remove" "member")
      (("" (USE "sum_nonneg" ("S" "remove(t!1, S!1)"))
        (("" (GROUND)
          (("1" (USE "sum_remove") (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_pos2| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "sum_bound4") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_neg| "" (SKOSIMP*)
    (("" (AUTO-REWRITE "remove" "member")
      (("" (USE "sum_nonpos" ("S" "remove(t!1, S!1)"))
        (("" (GROUND)
          (("1" (USE "sum_remove") (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_neg2| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "sum_bound3") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_zero| "" (SKOSIMP)
    (("" (USE* "sum_nonneg" "sum_nonpos")
      (("" (APPLY (REPEAT (THEN (SPLIT) (SKOLEM!) (INST?) (ASSERT)))) NIL
        NIL))
      NIL))
    NIL)
   (|sum_closure1| "" (SKOLEM + (_ "U!1" "f!1"))
    ((""
      (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]"
       :REWRITES ("sum_add" "sum_singleton") :EXCLUDE ("sum") :THEORIES
       ("sets[T]"))
      (("" (INST? -2) NIL NIL)) NIL))
    NIL)
   (|sum_closure2| "" (SKOLEM + (_ "U!1" "f!1"))
    ((""
      (AUTO-REWRITE "sum" "sum_emptyset" "rest" "remove" "member"
                    "nonempty?")
      (("" (INDUCT "S" :NAME "finite_set_induction_rest[T]")
        (("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)) NIL))
      NIL))
    NIL)
   (|sum_nnreal_is_nnreal| "" (SKOLEM!)
    (("" (REWRITE "sum_nonneg")
      (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|sum_npreal_is_npreal| "" (SKOLEM!)
    (("" (REWRITE "sum_nonpos")
      (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|sum_posreal_is_posreal| "" (SKOLEM!)
    (("" (REWRITE "sum_pos2")
      (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|sum_negreal_is_negreal| "" (SKOLEM!)
    (("" (REWRITE "sum_neg2")
      (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|sum_rat_is_rat| "" (SKOLEM!) (("" (REWRITE "sum_closure2") NIL NIL))
    NIL)
   (|sum_nnrat_is_nnrat| "" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)
   (|sum_nprat_is_nprat| "" (SKOLEM!)
    (("" (REWRITE "sum_npreal_is_npreal") NIL NIL)) NIL)
   (|sum_posrat_is_posrat| "" (SUBTYPE-TCC) NIL NIL)
   (|sum_negrat_is_negrat| "" (SKOLEM!)
    (("" (REWRITE "sum_negreal_is_negreal") NIL NIL)) NIL)
   (|sum_int_is_int| "" (AUTO-REWRITE-THEORY "integers")
    ((""
      (INDUCT-AND-SIMPLIFY "S" 1 "finite_set_induction_rest[T]" :DEFS NIL
       :REWRITES ("sum_emptyset" "sum"))
      NIL NIL))
    NIL)
   (|sum_npint_is_npint| "" (SKOLEM!)
    (("" (REWRITE "sum_npreal_is_npreal") NIL NIL)) NIL)
   (|sum_negint_is_negint| "" (SKOLEM!)
    (("" (REWRITE "sum_negreal_is_negreal") NIL NIL)) NIL)
   (|sum_nat_is_nat| "" (SKOLEM!)
    (("" (REWRITE "sum_nnreal_is_nnreal") NIL NIL)) NIL)
   (|sum_posnat_is_posnat| "" (AUTO-REWRITE-DEFS :EXPLICIT? T)
    (("" (ASSERT) (("" (SKOLEM-TYPEPRED) (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|sum_max_bound| "" (SKOSIMP)
    (("" (SKOLEM!)
      (("" (AUTO-REWRITE "card_remove" "member")
        (("" (USE "sum_bound" ("S" "remove(t!1, S!1)" "N" "N!1"))
          (("" (GROUND)
            (("1" (USE "sum_remove")
              (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (DELETE -1 2)
              (("2" (AUTO-REWRITE "remove") (("2" (REDUCE) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_min_bound| "" (SKOSIMP)
    (("" (SKOLEM!)
      (("" (AUTO-REWRITE "card_remove" "member")
        (("" (USE "sum_bound2" ("S" "remove(t!1, S!1)" "N" "N!1"))
          (("" (GROUND)
            (("1" (USE "sum_remove")
              (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (DELETE -1 2)
              (("2" (AUTO-REWRITE "remove") (("2" (REDUCE) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_0_non_neg| "" (SKOSIMP)
    (("" (USE "sum_min_bound") (("" (GROUND) NIL NIL)) NIL)) NIL)
   (|sum_0_non_pos| "" (SKOSIMP)
    (("" (USE "sum_max_bound") (("" (GROUND) NIL NIL)) NIL)) NIL)
   (|equal_sum_le| "" (SKOSIMP*)
    (("" (ASSERT)
      (("" (USE "sum_le" ("S" "remove(t!1, S!1)" "f" "f!1" "g" "g!1"))
        (("" (GROUND)
          (("1" (AUTO-REWRITE "member")
            (("1" (USE "sum_remove" ("f" "f!1"))
              (("1" (USE "sum_remove" ("f" "g!1"))
                (("1" (ASSERT)
                  (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (DELETE -1 2)
            (("2" (AUTO-REWRITE "remove" "member")
              (("2" (REDUCE) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|equal_sum_ge| "" (SKOSIMP)
    (("" (USE "equal_sum_le" ("f" "g!1" "g" "f!1"))
      (("" (REDUCE) NIL NIL)) NIL))
    NIL)
   (|sum_0_non_neg2| "" (SKOSIMP)
    (("" (USE "sum_0_non_neg")
      (("" (GROUND) (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|sum_0_non_pos2| "" (SKOSIMP)
    (("" (USE "sum_0_non_pos")
      (("" (GROUND) (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|sum_subset| "" (SKOSIMP)
    (("" (USE "sum_diff_subset" ("A" "A!1" "B" "B!1"))
      (("" (ASSERT)
        (("" (USE "sum_nonneg" ("S" "difference(B!1, A!1)"))
          (("" (GROUND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_subset2| "" (SKOSIMP)
    (("" (USE "sum_diff_subset" ("A" "A!1" "B" "B!1"))
      (("" (ASSERT)
        (("" (USE "sum_nonpos" ("S" "difference(B!1, A!1)"))
          (("" (GROUND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_order_sub| "" (SKOSIMP)
    (("" (USE "sum_subset" ("h" "h1!1"))
      (("" (ASSERT)
        (("" (USE "sum_le" ("S" "B!1" "f" "h1!1" "g" "h2!1"))
          (("" (GROUND)
            (("" (DELETE -1 -2 2) (("" (REDUCE) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_order_sub2| "" (SKOSIMP)
    (("" (USE "sum_subset2" ("k" "k1!1"))
      (("" (ASSERT)
        (("" (USE "sum_ge" ("S" "B!1" "f" "k1!1" "g" "k2!1"))
          (("" (GROUND) (("" (SKOLEM!) (("" (INST?) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_subset3| "" (SKOSIMP)
    (("" (USE "sum_diff_subset" ("f" "f!1" "A" "A!1" "B" "B!1"))
      (("" (ASSERT)
        (("" (USE "sum_zero" ("S" "difference(B!1, A!1)"))
          (("" (GROUND)
            (("" (DELETE -1 -2 2) (("" (GRIND) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  --------------050201060006020300050005--
  

How-To-Repeat: 

Fix: 
Fixed a minor typo.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools