Historique | Voir | Annoter | Télécharger (20,12 ko)
predicate 0BIT in sect 3.1
.
done first pass
done with arithmetic
done with soundness
Added 2 predicates in 4.1
graphs of basic functions
some graphs of basic functions
bit(l;x) function
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
characteristic functions
added basic template