Whose attitude? Mine, or that of the mathematicians who don't talk to
each other? Observe that my comment DID ALREADY start a conversation!
Now, to continue it: if (one of) the aim(s) of the QED project is to
computerize mathematics in such a way that MATHEMATICIANS use the
computerization, then we had better pay some attention to the sociology
of mathematics, I mean, to the way in which mathematicians actually
accomplish their work. The point of my "observation" is that most
mathematicians (the ones I know, and the ones Thurston writes about)
seem to feel that they are doing just fine as it is: they know how to
do their work and they aren't crying out for computer support. So if
we hope to avoid the fate of Principia Mathematica (on shelves gathering
dust), we need to think about how to do that.
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id GAA16661 for qed-out; Wed, 3 May 1995 06:12:20 -0500
Received: from gold.tc.umn.edu (root@gold.tc.umn.edu [128.101.115.11]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id GAA16653 for <qed@mcs.anl.gov>; Wed, 3 May 1995 06:10:47 -0500
Received: from dialup-1-33.gw.umn.edu by gold.tc.umn.edu; Wed, 3 May 95 06:10:37 -0500
X-Sender: inman002@gold.tc.umn.edu
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
To: ma_friesel@ccmail.pnl.gov
From: inman002@gold.tc.umn.edu (Eric Inman)
Subject: Probabilistic Proofs
Cc: qed@mcs.anl.gov
X-Mailer: <PC Eudora Version 1.4>
Message-Id: <2fa764ae435e002@gold.tc.umn.edu>
Date: Wed, 3 May 95 06:10:39 -0500
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 799510200.005
>One solution may be to create probablistic proofs for problems which are
>beyond the capabilities of an otherwise 'best' implementable proof engine.
>... I seem to recall reading something along the lines of such proofs, but
>I find no reference at hand.
Probabilistic proofs are mentioned on pp. 102,3 of "The Death of Proof,"
Scientific American, October, 1993.
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id MAA24467 for qed-out; Wed, 3 May 1995 12:53:45 -0500
Received: from altair (altair.mcs.anl.gov [140.221.2.7]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id MAA24462 for <qed@mcs.anl.gov>; Wed, 3 May 1995 12:53:37 -0500
From: Larry Wos <wos@mcs.anl.gov>
Date: Wed, 3 May 1995 12:53:36 -0500
Message-Id: <199505031753.MAA10998@altair>
To: qed@mcs.anl.gov
Subject: contact req.
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 799524829.000
Can somebody tell me wo to cntact by email and by phone on the
interest to use a theorem prover for the hardware verification,
secifically, the recent e-mal on BBD's? Thaks. LW
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id QAA28592 for qed-out; Wed, 3 May 1995 16:06:32 -0500
Received: from life.ai.mit.edu (life.ai.mit.edu [128.52.32.80]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id QAA28580 for <qed@mcs.anl.gov>; Wed, 3 May 1995 16:06:11 -0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA21379; Wed, 3 May 95 17:05:44 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI-4.10) id AA23164; Wed, 3 May 95 17:05:43 EDT
Date: Wed, 3 May 95 17:05:43 EDT
Message-Id: <9505032105.AA23164@spock>
To: rv_harris@ccmail.pnl.gov
Cc: pollack@cs.chalmers.se, ma_friesel@ccmail.pnl.gov, qed@mcs.anl.gov
In-Reply-To: rv_harris@ccmail.pnl.gov's message of Mon, 01 May 1995 10:31 -0700 (PDT) <01HPZI7DCEKM00004Y@pnl.gov>
Subject: Paper on reflection
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 799541782.000
Not to mention having to verify the operation of the hardware on which the C
code is running (as per the recent Pentium flap).
This seems orthogonal to whether we use C as the extension
language. Even if we used ML for extensions, the correctness of an
extension still assumes correctness of the hardware on which we are
ultimately running.
David
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id GAA13303 for qed-out; Thu, 4 May 1995 06:34:12 -0500
Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id GAA13293 for <qed@mcs.anl.gov>; Thu, 4 May 1995 06:34:03 -0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP-6.5) to cl; Thu, 4 May 1995 12:22:53 +0100
To: qed@mcs.anl.gov
Subject: Re: Paper on reflection
In-reply-to: Your message of "Wed, 03 May 1995 17:05:43 EDT." <9505032105.AA23164@spock>
Date: Thu, 04 May 1995 12:22:18 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:208250:950504112331"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 799596352.006
| Even if we used ML for extensions, the correctness of an extension still
| assumes correctness of the hardware on which we are ultimately running.
Of course, there is a dependence on the correctness of the implementation
language compiler and underlying hardware regardless of whether one is
interested in reflection.
The point is that computational reflection usually involves absorbing the
computer implementation of the logic into the logic's abstract description. By
contrast, in an LCF system, whatever the merits of the implementation, one can
give a simple, coherent account of what the logic is. For a QED-like effort
this seems important.
John.
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id DAA23207 for qed-out; Sat, 6 May 1995 03:54:15 -0500
Received: from tuminfo2.informatik.tu-muenchen.de (root@tuminfo2.informatik.tu-muenchen.de [131.159.0.81]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id DAA23202; Sat, 6 May 1995 03:54:06 -0500
Received: from sunjessen21 ([131.159.20.47]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26638-4>; Sat, 6 May 1995 10:52:38 +0200
Received: by sunjessen21.informatik.tu-muenchen.de id <460947>; Sat, 6 May 1995 10:52:23 +0200
From: Johann Schumann <schumann@informatik.tu-muenchen.de>
To: qed@mcs.anl.gov, wos@mcs.anl.gov
Subject: Re: contact req.
Cc: schumann@sunjessen21.informatik.tu-muenchen.de
Content-Length: 750
Message-Id: <95May6.105223mesz.460947@sunjessen21.informatik.tu-muenchen.de>
Date: Sat, 6 May 1995 10:52:12 +0200
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 799804985.005
Larry,
here in Germany is a group which uses THP's for hardware verification.
I give you the address and phone number of one member of the group.
He will certainly give you more details names of other persons
working in that area.
Thomas Kropf
Institut fuer Rechnerentwurf
Po Box 6980
76128 KARLSRUHE, Germany
email: kropf@ira.uka.de
Phone: +49-721-6084220
best regards
Johann Schumann
------------------------------------------------------------
Johann M. Ph. Schumann
Intellektik - AI Research Group at the Chair of Computer Architecture
Institut fuer Informatik
Technische Universitaet Muenchen
Augustenstr. 46 RGB
80290 Muenchen, Germany
email: schumann@informatik.tu-muenchen.de
------------------------------------------------------------
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id IAA10208 for qed-out; Thu, 18 May 1995 08:10:56 -0500
Received: from compu735.mathematik.hu-berlin.de (compu.mathematik.hu-berlin.de [141.20.18.102]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id IAA10197 for <qed@mcs.anl.gov>; Thu, 18 May 1995 08:10:48 -0500
Received: from kummer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP
(1.37.109.8/16.2/4.93/main) id AA08735; Thu, 18 May 1995 15:10:34 +0200
Received: from wega.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG)
id AA26918; Thu, 18 May 95 15:10:14 +0200
Date: Thu, 18 May 95 15:10:14 +0200
From: dahn@mathematik.hu-berlin.de (Bernd Ingo Dahn)
Message-Id: <9505181310.AA26918@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: QED Workshop 2 - Cooperation of Automated and Interactive Theorem Provers
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 800805456.022
This is a brainstorming request in preparation of the QED Workshop 2
in Bialystok/Poland in July.
I agreed with the organizers to lead a discussion on
Cooperation of Automated and Interactive Theorem Provers
at the workshop. In the introduction I shall report on the cooperation
experience gained in the german Schwerpunktprogramm Deduktion
(provers and people).
I shall also report on setting up an Internet mail server to provide
distant provers with natural language proof presentations.
However, there are certainly a lot of other useful things to do
concerning cooperation.
Therefore, if you have any idea on the subject - possibly even vague or
unrealistic - please, send them to
Bernd, Ingo Dahn,
Institut fuer Reine Mathematik
der Humboldt-Universitaet
Ziegelstr. 13a
D-10099 Berlin
Please, note that this is not! to start a network discussion now but only
for the benefit of the workshop. So, don't expect any comments for now.
Best regards
Ingo Dahn
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id GAA02656 for qed-out; Mon, 22 May 1995 06:47:42 -0500
Received: from cksr.ac.bialystok.pl (cksr.ac.bialystok.pl [193.59.8.46]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id GAA02641 for <qed@mcs.anl.gov>; Mon, 22 May 1995 06:43:03 -0500
From: trybulec@cksr.ac.bialystok.pl
Date: Mon, 22 May 95 13:41 MED
Message-ID: <9505221347.AA09578@cksr.ac.bialystok.pl>
To: qed@mcs.anl.gov
Content-Length: 4089
Content-Type: binary
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.008
The approach [2] (according to Harrison's classification) is standard in
Mizar. The inverse is treated exactly as John wrote:
1. The definition of inverse is (I edited it slightly
to make it understandable outside the context, the same goes for
other examples)
definition
let x be Real;
assume x<>0 ;
func x" -> Real means
x * it = 1 ;
end;
One can justify that 0 * (0/0) = 0 by reference to the theorem REAL_1:23:
x*y=0 iff (x=0 or y=0)
i.e. Mizar accepts
0 * (0/0) = 0 by REAL_1:23;
as a correct inference.
(actually in Mizar we use rather \cdot than *).
We say that a definition is permissive if it allows for assigning
some arbitrary value outside its domain.
( We borrowed the name from W{\l}adys{\l}aw Turski, he used it for
incomplete specification.)
If I correctly recall
permissiveness is used in Excheck for the abstraction operator, one
can use
{ x : P[x] }
without any restriction, but to infer
y \in { x : P[x] } implies P[y]
one have to prove earlier that there exists a set A such that
P[x] implies x \in A
(I doubt if the syntax I use is really the Excheck syntax, sorry;
I just like this example).
However, the approach [1] gives quite often better results. We have
changed (while revising the Mizar library) a number of definition
that were originally permissive, that enabled enhancement of the
library:
The definition of the result of the application of a function f to
an arbitrary x was originally permissive:
definition let f,x;
assume x \in dom f;
func f.x -> Any means
[x,it] \in f;
end;
(square brackets we use for ordered pairs)
It is now:
definition let f,x;
func f.x -> Any means
[x,it] \in f if x \in dom f otherwise it = 0;
end;
with the second definition we can simplify the original theorem FUNCT_1:23
x \in dom f & f.x \in dom g implies (g \cdot f).x = g.(f.x);
to
x \in dom f implies (g \cdot f).x = g.(f.x);
( \cdot stands for the composition of functions )
It is very important in Mizar to get more concise theorems.
To use a theorem in a proof we have first to prove
its premises, and we get an abundance of trivial facts (something is
non empty, something belongs somewhere) that makes the proof obscure
and takes a lot of work (it takes in some proofs more than 50 per cent of
the text).
Also, after such simplification some theorems coincide, and may be removed
from the library (and data base as well). And the size of the data base
is a critical parameter.
Then, why the second approach ?
John pointed out that the first one
>>> gives you strange "accidental" theorems
and the second one gives
>>> gives fewer convenient theorems, but also fewer accidental ones
That's right, but this is a minor point, nobody is pressed to formulate
such theorems. I would like to call them "obscene" (or it is too
strong ? then "shocking", "indecent" ? ... English native speakers
should decide; we need a technical term for them, I hope that "obscene"
might be good, because it is rarely used as a scientific term).
Teaching Mizar I often use the slogan
" you can divide by zero, but you don't do it"
or more general
"even if the language allows for obscenities, it does not mean
that the user should use them"
and of course it is just nothing in comparison to the Automath restaurant,
could you imagine what will be served in it ?
What is more important, quite often it is not clear which value is
convenient.
One can put
0" = 0, to get (-x)" = -x", or
0" = 1, to get x/y = 0 implies x = 0 or
0" = +\infty (the most reasonable if system allows for infinite values).
Therefore we encourage users to use permissiveness (if they have no
precise preference). After some experience we change to non permissive
definition, while revising the library. If it is possible.
Mizar is a typed language and if f is a finite sequence of elements of
a non empty set D, then the concept of
the k-th member of f
must be permissive (if it is supposed to be an element of D).
To summarize, the general approach is the approach [2], when possible
and useful we use approach [1].
Andrzej Trybulec
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id IAA03302 for qed-out; Mon, 22 May 1995 08:30:04 -0500
Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id IAA03297 for <qed@mcs.anl.gov>; Mon, 22 May 1995 08:29:56 -0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP-6.5) to cl; Mon, 22 May 1995 14:27:46 +0100
To: qed@mcs.anl.gov
In-reply-to: Your message of "Mon, 22 May 1995 13:41:00 -0400." <9505221347.AA09578@cksr.ac.bialystok.pl>
Date: Mon, 22 May 1995 14:27:18 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:171830:950522132813"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.020
Andrzej Trybulec writes:
| If I correctly recall
| permissiveness is used in Excheck for the abstraction operator, one
| can use
| { x : P[x] }
| without any restriction, but to infer
| y \in { x : P[x] } implies P[y]
| one have to prove earlier that there exists a set A such that
| P[x] implies x \in A
Yes, I meant to remark on this kind of problem with approaches [1] and [2]. In
the HOL real analysis theories we have various higher order operators for
"limit", "derivative", "integral" and so on. These are usually applied to
lambda terms giving a uniform treatment of variable binding constructs (see QED
passim.) Thus:
|- lim x_n = l
n->oo
is really a gloss for something like:
|- LIM_INFINITY (\n. x_n) = l
Because of the approach I've taken to undefinedness, theorems like this are
weaker than they look. LIM_INFINITY returns a value on any sequence, whether
convergent or not, and we can't a priori rule out the possibility that it could
give "l" on a nonconvergent sequence. Thus the above does *not* imply that
"x_n" is convergent. In practice then, I tend to use the stronger property "x_n
tends to l" instead of "the limit of x_n is l". For example, the theorem about
the limit of a sum is (verbatim; "!" means "for all", "/\" means "and", "==>"
means "implies" and "\" means "lambda"):
|- !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x(n) + y(n)) --> (x0 + y0)
On the whole this works well, but has quite poor compositionality properties;
for example dealing with nontrivial differential equations in these terms is a
bit tiresome!
John.
Received: from linus.mitre.org (linus.mitre.org [129.83.10.1]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id JAA04454 for <owner-qed@mcs.anl.gov>; Mon, 22 May 1995 09:37:05 -0500
Received: from triad.mitre.org (triad.mitre.org [129.83.10.97]) by linus.mitre.org (8.6.12/8.6.12) with ESMTP id KAA14593 for <owner-qed@mcs.anl.gov>; Mon, 22 May 1995 10:37:03 -0400
Received: from localhost (jt@localhost) by triad.mitre.org (8.6.12/8.6.12) with SMTP id KAA02763 for <owner-qed@mcs.anl.gov>; Mon, 22 May 1995 10:36:07 -0400
Message-Id: <199505221436.KAA02763@triad.mitre.org>
X-Authentication-Warning: triad.mitre.org: jt owned process doing -bs
X-Authentication-Warning: triad.mitre.org: Host localhost didn't use HELO protocol
To: owner-qed@mcs.anl.gov
In-reply-to: Your message of "Mon, 22 May 1995 13:41:00 -0400."
<9505221347.AA09578@cksr.ac.bialystok.pl>
Date: Mon, 22 May 1995 10:36:06 -0400
From: "F. Javier Thayer" <jt@linus.mitre.org>
X-UIDL: 801410893.022
It is particularly important in much of mathematics to refer of the
domain of a function. For instance, much of the theory of unbounded
operators on infinite dimensional spaces, as currently formulated,
uses in a critical way the domains of these operators. Are we to
reformulate the theory to accomodate some particular vision of how
mathematics should be done?
This is not an isolated example. Functions with essential
discontinuities (that is without limits at these points) are really
best though of as being undefined at those points.
Javier
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id NAA09255 for qed-out; Mon, 22 May 1995 13:31:41 -0500
Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id NAA09246 for <qed@mcs.anl.gov>; Mon, 22 May 1995 13:31:36 -0500
Received: from thunder.cli.com by cli.com (4.1/SMI-4.1)
id AA16704; Mon, 22 May 95 13:31:03 CDT
From: kaufmann@CLI.COM (Matt Kaufmann)
Received: by thunder.cli.com (4.1) id AA04663; Mon, 22 May 95 13:31:03 CDT
Date: Mon, 22 May 95 13:31:03 CDT
Message-Id: <9505221831.AA04663@thunder.cli.com>
To: holmes@catseye.idbsu.edu
Cc: moore@CLI.COM, qed@mcs.anl.gov
In-Reply-To: <199505181835.NAA19932@antares.mcs.anl.gov> (message from Randall Holmes on Thu, 18 May 1995 12:39:59 -0600)
Subject: Re: Undefined terms
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.054
Hi --
Regarding your query about "undefined terms":
>> I'd like to hear
>> what is done in actual systems.
Here is a brief account of what is done in Nqthm (sometimes called the
"Boyer-Moore" prover) and in ACL2 (its successor).
In both Nqthm and ACL2, we take Harrison's approach [1]: ``Resolutely give
each partial function a convenient value on points outside its domain.'' Users
have found this approach to be really helpful in cutting down on the number of
cases and the number of lemmas required, and only rarely has there seemed to be
an issue about *which* convenient value to take, in the sense that Trybulec
mentioned:
>> What is more important, quite often it is not clear which value is
>> convenient.
>> One can put
>> 0" = 0, to get (-x)" = -x", or
>> 0" = 1, to get x/y = 0 implies x = 0 or
>> 0" = +\infty (the most reasonable if system allows for infinite values).
At one point, however, we considered moving more towards Harrison's approach
[2] in ACL2: ``Give each partial function some arbitrary value outside its
domain.'' This turned out to greatly complicate the proof burdens on users.
In particular, one of our colleagues who uses ACL2 daily has commented that the
reversion of ACL2 to an Nqthm-like approach (i.e., [1]) has greatly helped him
in his work.
Below is a simple example that illustrates the potential advantage of [1]
(assignment of convenient values) over [2] (use of arbitrary, undefined values)
in our context. This example is sufficiently simple that one could reasonably
argue that other approaches would solve it more simply, for example Harrison's
[3], using types. However, our goal here is simply to illustrate advantages of
[1] over [2].
Consider the following problem. Define a function that sums a list of natural
numbers, and then prove the following theorem: the sum of the result of
appending two lists together is the same as adding the sums of each list. In
ACL2 (in fact, in Common Lisp) one can define the sum of a list of natural
numbers as follows. Note: informally speaking, the "(declare ... :guard ...)"
expression below specifies that only those x that are lists of natural numbers
are "in the domain" of the function SUMLIST.
[Here and subsequently, semicolons (;) indicate comments to the end-of-line.]
(defun sumlist (x)
(declare (xargs :guard (nat-listp x))) ; x "should" be a list of naturals
(if (endp x) ; same as (atom x), but probably more efficient
0
(+ (car x)
(sumlist (cdr x)))))
Now the theorem we want to prove may be stated as follows. Note that it has no
hypotheses, even though we might only "intend" it to hold in the case that x
and y are lists of natural numbers. However, ACL2 uses rewriting heavily, and
the elimination of hypotheses in rewrite rules such as the following is helpful
in subsequent proofs.
(defthm sumlist-append ; name of theorem
(equal (sumlist (append x y)) ; left side of rewrite rule
(+ (sumlist x) (sumlist y)))) ; right side of rewrite rule
ACL2 has no trouble proving this theorem automatically, without any apparent
consideration of cases arising from adding non-numbers (which by the way are
treated as 0 for that purpose, i.e., 0 is the conveniently chosen value for
points outside the "domain" of +). However, in a previous version of ACL2 we
used approach [2], and the proof required the following lemmas.
(defthm sumlist-rationalp
;; If x is a list of naturals, then its sum is a rational number.
(implies (nat-listp x)
(rationalp (sumlist x)))
:rule-classes :type-prescription)
(defthm nat-listp-implies-true-listp
;; If x is a list of naturals, then it is a null-terminated list.
(implies (nat-listp x)
(true-listp x))
:rule-classes :forward-chaining)
(defthm nat-listp-append
;; If x and y are lists of naturals, then their concatenation is too.
(implies (and (nat-listp x)
(nat-listp y))
(nat-listp (append x y)))
:rule-classes :type-prescription)
The discovery of these lemmas required, unfortunately, some expertise in using
the system. Note also the obscure "rule-classes". We'll spare you the details
(but can send individuals a more extensive write-up upon request.) Moreover,
the final theorem *requires* hypotheses:
(defthm sumlist-append
(implies (and (nat-listp x)
(nat-listp y))
(equal (sumlist (append x y))
(+ (sumlist x) (sumlist y)))))
This kind of complicatation was sufficiently common to cause us to make major
changes in the ACL2 logic and implementation, the result being a system that
bears considerably more resemblance to its predecessor, Nqthm, than had been
the case.
Matt Kaufmann
J Moore