1	import Base
2	import ./containers/intrusive_doubly_linked_list/proof.bend as IntrusiveList
3	import ./containers/dlist_iterator/proof.bend as IteratorComponents
4	import ./containers/balanced_search_tree/components.bend as TreeMapComponents
5	import ./END_TO_END.bend as End
6	import ./lib/lemmas/proofs/public_trace.bend as LruTrace
7	import ./math/proof.bend as Math
8	import ./containers/hash_table/proof.bend as HashTable
9	import ./containers/lru/proof.bend as Lru
10	import ./containers/doubly_linked_list/proof.bend as Dll
11	import ./containers/balanced_search_tree/proof.bend as TreeMap
12	import ./containers/bitlist/proof.bend as Bitlist
13	
14	# Root gate. Checks END_TO_END.bend (and through it every proofs/<id>.bend
15	# entry), the retained LRU's trace refinement (lib/lemmas/proofs/public_trace),
16	# the math library, the refinements of the hash map, the LRU cache, the doubly
17	# linked list, the indexed TreeMap and the bit list, and the TreeMap's
18	# component laws.