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

No Subject

Michele,

Shankar sent me some further comments:

1. In the prop theorem, the x>0 term is redundant, since that's what
   posnat means.

2. You can help the prover by modifying the definition of doublefatt to
        doublefatt(x) : RECURSIVE posnat =
	      IF x <= 1 THEN 1
	      ELSE x*doublefatt(x-2)
	      ENDIF
         MEASURE x
   This has the same semantics, but in this form the top-level condition
   completely determines whether the function recurses.

   With this change, the proof can be simplified to

   ("" (INDUCT-AND-SIMPLIFY "x") (EXPAND "doublefatt" 1 1) (GRIND))

Sam