ANP={q| q is an algorithmic decision problem. Let q(n) be the computing function
of q using n as the problem argument. If given additional information c,
the case that q(n)=1 can be computed in P-time.
}

Specifically, the semantics of ANP suggests that a P-time function q'(n,c) is
given (otherwise, q won't be well defined), and:
q'(n,c): S×S ->{0,1}, where S={0,1}^N.
That q'(n,c) returns 1 means q(n)=1 (0 means c is not decisive).

Therefore, q(n) can be generalized in this C-like pseudo-program when c is
necessary:
bool q(n) {
begin= get_begin(n);
end = get_end(n);
for(c=begin; c!=end; c=next(c)) {
if(q'(n,c)) return 1;
}
return 0;
}

Note that the above is attributed as generalized is because the unknown
information c has O(2^N) possibilities (worst case), each of them have to be
explicitly generated and tested. There may be doubt that one possibility of c may contain information about another case (or, can q' return any suggestive
information?). The short answer is: it does not matter because the c asked by
ANP may be a pure bit-string that each bit is independent.

ANP is defined the kind of problem that O(2^N) unknown independent possibilities
HAS TO BE FIXED to compute in P-time (worst case). This is the essence of this
proof. In applications, a specific problem in doubt may need to show it does
require c information (O(2^N) possibilities) to fit in ANP, not easy (hope I am
wrong), but this is not the problem of ANP (this part is indirectly covered by
NP and NPC theory).

----------------
Also, as posted in C/C++ group, I would like to say that program has to be
able to show it is correctly (optimally provable) written for the problem.
I.e. the application of the language may include theorem proving.
Sub-goals like expressiveness, 'cleanness' make correctness proving difficult
(esp. error handling is considered)... If something is good, something has to
be considered not good. Every new feature makes others less reusable.