Added bjax-3 and bnry-3, updated proofs