8 lines (6 loc) · 424 Bytes

proofs

Proofs of simple mathematical properties

binary.v Inductive proof that given binary to unary conversion holds for:
- bin2nat(code + 1) ≡ bin2nat(code) + 1
pumping.v Proof of Pumping Lemma for regular expressions.

Better use with Emacs Proof General. my .emacs