Add b-tree example

Author: lorin

README.md

@@ -135,6 +135,7 @@ Ideally these will be moved into this repo over time.
 | [Petri Nets](https://github.com/elh/petri-tlaplus)                                                                                | Instantiable Petri Nets with liveness properties                                                                                          | Eugene Huang                                                               |          |             |     ✔     |         |          |
 | [CRDT](https://github.com/JYwellin/CRDT-TLA)                                                                                      | Specifying and Verifying CRDT Protocols                                                                                                   | Ye Ji, Hengfeng Wei                                                        |          |             |     ✔     |         |          |
 | [Azure Cosmos DB](https://github.com/tlaplus/azure-cosmos-tla)                                                                    | Consistency models provided by Azure Cosmos DB                                                                                            | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe            |          |             |     ✔     |    ✔    |          |
+| [B-trees](https://github.com/lorin/btree-tla)                                                                                     | Operations on B-trees. Includes a refinement mapping to a key-value store spec.                                                           | Lorin Hochstein                                                            |          |             |     ✔     |         |          |
 
 ## License
 The repository is under the MIT license and you are encouraged to publish your spec under a similarly-permissive license.