.
corrected example 5
added tech report folder
proof of minimisation lemma, in appendic completeness
basic functions
predicate 0BIT in sect 3.1
done with completeness
fixed other basic axioms
done first pass
done with arithmetic
done with soundness
Added the completeness proof sketch
down to 12 pages
Added 2 predicates in 4.1
graphs of basic functions
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