Here is the required proof:

http://www.dcproof.com/AddFunctionNEW.proof

Dan

--- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@...> wrote:
>
> Thomas,
>
> Thanks for bringing this to my attention! The proof in question
(at
> the DC Proof website) was written with an old version of DC Proof.
> Currently, selection criteria for a subset s may not refer to s
> itself. I discovered that if you allow such selections, as older
> versions did, you would be able to "prove" that all sets are
empty!
> So it was back to the drawing board, as they say.
>
> I will try to rewrite this important proof using the revised
Subset
> Rule.
>
> Regards,
> Dan
>
>
> --- In dcproof@yahoogroups.com, Thomas Heye <1910-131@> wrote:
> >
> > Hi list,
> > looking at the proof regarding addition of natural numbers, it
was
> > stated that the subset rule had been used-- in particular the
set s
> > being constructed was referenced in the selection criteria.
> >
> > Maybe somebody can help me; what follows is the fragment of a
> prrof I
> > started. It's strange that the premise rule dialog accepted the
> > selection criteria for the set s; nevertheless, when I entered
the
> > part after ")a,b= in n2" in the subset dialog, DCProof complained
> > about an "invalid reference to s".
> >
> > Of course, I can work on the proof with that new premise, but
I'm
> not
> > very fond of too many "nested blocks".
> >
> > Best regards,
> >
> > Thomas
>