some graphs of basic functions
bit(l;x) function
basic function addition
added conclusion
.
intro revised (in progress)
added vl
Completeness: recursion step.
completed the list of Basic axioms, following Buss, in the appendix
Revised the definitions at the beginning of sect 4, and added after Def 14 a comment about B^i and integer positive formulas.
Modified lemma 19 on well-typed proofs, and gave a proof sketch.
Modified sequent calculus rules (weakening in axioms)
B^i sequent calculus
added polynomial induction definition
added the sequent calculus rules and a free-cut elimination theorem
witness functions
characteristic functions
predicative minimisation
corrected polynomial checking lemma
+ 1 reference
preliminaries: definitions PH
added in preliminaries the polychecking lemma
added definitions mubc
added basic template
added csl17 dir