The following is a small proof in Nuprl
with the extraction clauses
shown explicitly. The system does not produce the comments (* 
*);
we include them for illustrative purposes only.
In the interest of condensing the presentation we also elide hypothesis lists wherever possible.
,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top (* term_of(thm) extracted *) | |>> all x,y:int.(x=y in int)|some z:int.~(z=0 in int)#(x+z=y | | in int | | | |BY quantifier (* ext \x.\y.e1 (quantifier tactic does | | intro twice) *) | |1* 1. x:(int) | | 2. y:(int) | | >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))| | (* ext e1 *) | |2* >> (int) in U1 | | | |3* >> (int) in U1 | '------------------------------------------------------------'
The rule quantifier is a tactic , a user--defined rule of inference, which successively applies the intro rule to each universal quantifier; in this case it performs two applications. This tactic was written by a user of the system and must be loaded as an ML object to be used; in general it would not be available. See the following chapter for more on tactics. The extracted term is a function which, given any values for x and y, will give a proof of the body; this corresponds to the intuitive meaning of all and justifies its definition as a dependent function. Note that e1 is the term extracted from the first subgoal; the next window shows the proof of this subgoal.
,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 (* e1 extracted *) | |1...2. | |>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int)) | | | |BY seq (x=y in int)|~(x=y in int) new E (* ext \E.e3(e2) *) | | | |1* 1...2. | | >> (x=y in int)|~(x=y in int) (* ext e2 *) | | | |2* 1...2. | | 3. E:(x=y in int)|~(x=y in int) | | >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))| | (* ext e3 *) | '------------------------------------------------------------'
The seq rule extracts a function which in effect substitutes the proof of the seq term, e2, for each instance of its use in e3 (under the name E).
,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 1 (* e2 extracted *) | |1...2. | |>> (x=y in int)|~(x=y in int) | | | |BY arith (* ext int_eq(x;y;inl(axiom);inr(axiom)) *) | | | |1* 1...2. | | >> x in int | | | |2* 1...2. | | >> y in int | | | |3* 1...2. | | >> x in int | | | |4* 1...2. | | >> y in int | '------------------------------------------------------------'
The arith decision procedure produces the int_eq term, a decision procedure for equality on the integers.
,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 (* e3 extracted *) | |1...2. | |3. E:(x=y in int)|~(x=y in int) | |>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int)) | | | |BY elim 3 (* ext decide(E;l.e4;r.e5) *) | | | |1* 1...3. | | 4. l:(x=y in int) | | >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))| | (* ext e4 *) | |2* 1...3. | | 4. r:~(x=y in int) | | >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))| | (* ext e5 *) | '------------------------------------------------------------'
The elim rule for disjoint unions produces a decide term. In the next frame the term l is extracted from the first subgoal because our goal is exactly l (the actual proof of this subgoal is not shown but is carried out using the rule hyp 4).
,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 1 (* e4 extracted *) | |1...3. | |4. l:(x=y in int) | |>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int)) | | | |BY intro left (* ext inl(e6) *) | | | |1* 1...4. | | >> (x=y in int) (* ext e6==l (follows by hyp 4) *) | | | |2* 1...4. | | >> some z:int.~(z=0 in int)#(x+z=y in int) in U1 | '------------------------------------------------------------'
In the next frame r is extracted for the same reason as l is above.
,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 2 (* e5 extracted *) | |1...3. | |4. r:~(x=y in int) | |>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int)) | | | |BY intro right (* ext inr(e7) *) | | | |1* 1...4. | | >> some z:int.~(z=0 in int)#(x+z=y in int) (ext e7 *) | | | |2* 1...4. | | >> ((x=y in int)) in U1 | '------------------------------------------------------------'
In the next frame, since some is defined to be a dependent product we extract a pair consisting of an element of the integers, y-x, and a proof, e8, that the proposition is true for this element. This corresponds to the desired meaning of some.
,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 2 1 (* e7 extracted *) | |1...3. | |4. r:~(x=y in int) | |>> some z:int.~(z=0 in int)#(x+z=y in int) | | | |BY intro y-x (* ext <y-x,e8> *) | | | |1* 1...4. | | >> y-x in (int) | | | |2* 1...4. | | >> ((y-x=0 in int)->void)#(x+y-x=y in int) (* ext e8 *)| | | |3* 1...4. | | 5. z:(int) | | >> (~(z=0 in int)#(x+z=y in int)) in U1 | '------------------------------------------------------------'
The product intro produces a pair consisting of proofs of the two subgoals. Although the proof is not shown here, subgoal 2 can be seen to follow trivially by arith.
,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 2 1 2 (* e8 extracted *) | |1...3. | |4. r:~(x=y in int) | |>> ((y-x=0 in int)->void)#(x+y-x=y in int) (* ext <e9,e10>*)| | | |BY intro | | | |1* 1...4. | | >> (y-x=0 in int)->void (* ext e9 *) | | | |2* 1...4. | | >> x+y-x=y in int (* ext e10==axiom (follows by arith)*)| '------------------------------------------------------------'
In the next frame we see that
hypotheses 4 and 5 contradict each other. The system somewhat
arbitrarily extracts (
v0.any(v0))(r(axiom))
from this (we could extract anything
we desired from a contradiction).
,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 2 1 2 1 (* e9 extracted *) | |1...3. | |4. r:~(x=y in int) | |>> (y-x=0 in int)->void | | | |BY intro new f (* ext \f.e11 *) | | | |1* 1...4. | | 5. f:y-x=0 in int | | >> void (* ext e11==(\v0.any(v0))(r(axiom)) | | (from a contradiction)*)| | | |2* 1...4. | | >> (y-x=0 in int) in U1 | '------------------------------------------------------------'
We could now have the following session with the evaluator . What follows has additional white space (spaces and carriage returns) to improve readability.
,------------------------------------------------------------, |P>eval | |E>term_of(thm);; | |\x.\y.(\E.decide(E;l.inl(l); | | r.inr(<y-x,<\f.(\v0.any(v0))(r(axiom)),axiom>>))) | | (int_eq(x;y ;inl(axiom);inr(axiom))) | |E>term_of(thm)(7)(7);; | |inl(axiom) | |E>term_of(thm)(7)(10);; | |inr(<10-7,<\f.(\v0.any(v0))(axiom(axiom)),axiom>>) | |E>let p1 = \x.spread(x;u,v.u);; | |\x.spread(x;u,v.u) | |E>let d = \y.decide(y;u.p1(u);u.p1(u));; | |\y.decide(y;u.p1(u);u.p1(u)) | |E>d(term_of(thm)(7)(10));; | |3 | '------------------------------------------------------------'
To terminate an eval session type 
.