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

help, !



Hi!

I have problems with 'expanding' recursive
definitions. get the message: 
"Error: the assertion (EVERY #'CDR BINDINGS) failed.
  [condition type: SIMPLE-ERROR]"


here is the example:
___________________________________________________________
test : THEORY

  begin

   regs : TYPE+;
   links : TYPE+;


   IMPORTING finite_sets[links]


   new_reg(r_set:set[regs]) : regs = 
            epsilon(difference(fullset[regs],r_set))

   rec_func(l_set:finite_set[links],r_set: set[regs]) : 
	      RECURSIVE set[regs] = 
	IF empty?(l_set) THEN emptyset[regs]
	ELSE (
	  LET one:links = epsilon[links](l_set),
              nr: regs = new_reg(r_set) IN
          add(nr,rec_func(remove(one,l_set), add(nr,r_set)))
	)
	ENDIF
    MEASURE card(l_set)

    try: LEMMA FORALL(l_set:finite_set[links],r_set:set[regs]) :
	    (nonempty?(l_set) and 
            nonempty?(difference(fullset[regs],r_set)))
	        IMPLIES nonempty?(rec_func(l_set,r_set))

    
end test
_____________________________________________________

when trying to prove "try", I get the error message
if the first prover command was (expand "rec_func").
The proof can be completed using a different sequence
of commands.

Is there any common restriction on when to use 'expand'?
I get similar error messages almost every time i'm
using recursive definitions.

thanks a lot!

_____________________________________

Ela Teica
DDEL Lab,
Univ of Cincinnati.


Don`t be superstitious; it brings bad luck!:)

____________________________________