Re: beginner's problem

[John Hoffman <hoffman@securecomputing.com>]

You added a t to fac_loop in thm4.

John


> 
> I'm sure this is something very basic.
> Here are some definitions in my pvs file.
> 
>    factorial(x:nat): RECURSIVE nat = 
> 	   IF x = 0 THEN 1 ELSE x * factorial(x-1) ENDIF
> 		   MEASURE x 
> 
>    fac_loop(x:nat, y:nat): RECURSIVE nat =
>     IF x = 0 THEN y ELSE fac_loop(x - 1, x * y) ENDIF
>     MEASURE x
> 
> I could prove this theorem:
> 
>    fact_thm3: THEOREM
>          (FORALL (m:nat, n:nat): fac_loop(m, n) = n * fac_loop(m, 1)
> 
> But when I added this theorem...
> 
>    fact_thm4: THEOREM (FORALL (m:nat): factorial(m) = fact_loop(m, 1))
> 
> I get this parse-error message:
> 
>    Expecting an expression
>    No resolution for fact_loop with arguments of types:
>      m : naturalnumbers.nat
>      1 : integers.posint
> 
> I've spent quite a while trying to figure out what's going on, but
> can't.  Please advise.
> 
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> Steven D. Johnson               net: sjohnson@cs.indiana.edu
> Computer Science Department     tel: 812-855-2567
> Indiana University              fax: 812-855-4829
> Bloomington, IN 47405-4101      www: via http://www.cs.indiana.edu
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>

---

• References:
  • beginner's problem
    • From: Steve Johnson <sjohnson@cs.indiana.edu>

• Prev by Date: beginner's problem
• Next by Date: Re: PVS License Agreement
• Prev by thread: Re: beginner's problem
• Next by thread: license
• Index(es):
  • Date
  • Thread