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



[Non-text portions of this message have been removed]