Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4); Fri, 8 Jan 1993 22:55:35 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13840;
          Fri, 8 Jan 93 13:30:00 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA13833; Fri, 8 Jan 93 13:29:52 -0800
Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA15131;
          Fri, 8 Jan 93 13:36:58 -0800
From: weiss@edu.uidaho.cs.leopard (P. Andrew Weiss)
Message-Id: <9301082136.AA15131@leopard.cs.uidaho.edu>
Subject: Quick help
To: info-hol@edu.uidaho.cs.ted (HOL mailing list)
Date: Fri, 8 Jan 93 13:36:57 PST
Full-Name: P. Andrew Weiss
Organization: Laboratory for Applied Logic
Mailer: Elm [revision: 66.33]

Anyone know a quick and easy way to prove the following goal?

g("!n. ~((SUC n) MOD (SUC(SUC 0) = n)");;

I'm running up against a mental block, as I always seem to do
when I try to prove anything with DIV and MOD.

Phil.

--
P. Andrew Weiss                 Laboratory for Applied Logic
weiss@leopard.cs.uidaho.edu     University of Idaho
weiss872@snake.cs.uidaho.edu    Moscow, ID  83843

I can't speak for myself even, so don't assume I'm speaking for
anyone else either.