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

[PVS-Help] using modulo_arithmetic




Hi, I'm having trouble proving the following theorem using the
modulo_arithmetic theory.  

	modding: THEOREM (forall (b: posnat), (x: nat):
		rem(b+1)(x + b) = 
			if rem(b+1)(x) = 0 then 
				b 
			else 
				rem(b+1)(x) - 1 endif)

I've simplified it to some extent but seem to be overlooking the
crucial property/technique for 'rem' that would allow me to complete
the proof.  Does anyone have a tip on how to proceed?

Thanks,
Rob