This file is intended a proof that ℙ≠ℕℙ. The contents may be updated anytime.
https://sourceforge.net/projects/cscall/files/MisFiles/PNP-proof.txt/download

Algorithmic problem::= The kind of problem that the size (length) of the
argument of the problem is variable, so that the steps of computation can
be expressed in asymptotic approximation.

ANP::= Set of algorithmic (decision) problems that the 'yes' answer can be
verified in P-time from O(2^N) possible candidates of certificates, where N
is the length of the problem's argument.

Precisely, ANP is a set of 3-tupple <ProblemArgs, Certificate, Verify> that
can be computed by a pseudo-C program template npf(n):

ProblemArgs::= Problem arguments
Certificate::= Set of certificate. #Certificate= O(2^#ProblemArgs).
(three access methods for iterating elements of Certificate
are required, see npf(n))
Verify::= A P-time decision function v:Certificate -> {0,1}

bool npf(ProblemArgs n) {
Certificate c,begin,end;
begin= get_begin_certificate(n);
end = get_end_certificate(n);
for(c=begin; c!=end; c=next(c)) { // O(2^|n|) loop
if(v(c)) return true; // v(c), the verification is in P-time
}
return false;
}

Note: If the C-code is not too fancy and close to Assembly, C-code can
denote the same thing as TM. Another reasons using C-code: 1. The
'false' answer of NDTM is visible in procedure npf(n). 2. The steps
of v(c) is not really restricted in the NDTM model, it can even run
indefinitely because NDTM runs in 'parallel'.
Note: The for loop in npf(n) may include nested loops for sets like
S=S1xS2xS3x... as implied in NDTM model.

----------------------------------------------------------------------------
This proof uses pseudo-C program to prove ℙ≠ℕℙ by contradiction. Technical
details are long and omitted.

// [Syn] Function sat(Prog prog, int n) decides whether or not prog(x) is
// satisfiable for x<=n. prog(x) is assumed a P-time function.
//
// [Ret] 1, if ∃c, c<=n, prog(c)==1
// 0, otherwise
//
// Prog::= pseudo-C Program
//
bool sat(Prog prog, int n) { // n>=0
for(int c=0; c<=n; ++c) {
if(prog(c)) return 1;
}
return 0;
}

If sat(..) is a P-time function, then u(x) will also be a P-time funtion:

bool u(int x) {
return !sat(u,x);
}

But, from definition of u(..), we will have:
u(0)==1 -> sat(u,0)==0 -> u(0)==0 // contradictory
u(1)==1 -> sat(u,1)==0 -> u(0)==0 and u(1)==0 // contradictory
...
u(x)==1 -> sat(u,x)==0 -> u(0)==0 and u(1)==0 and ... u(x)==0 // contradictory

Therefore, if sat(..) is a P-time function, then sat(..) will encounter
undecidable (term from Halting Problem) cases. Thus, sat(..) cannot be a
P-time function.
Since Problem(sat)∈ANP and Problem(sat)∉ℙ, therefore, ANP ⊈ ℙ. If ANP==ℕℙ,
then, ℕℙ≠ℙ.
QED. ----------------------------------------------------------------