1	import Base
2	import ./invariants.bend as Inv
3	import ./map_routing.bend as R
4	import ./map_delete_routes.bend as D
5	import ./map_delete_prefix.bend as P
6	import ./map_string_prefix.bend as Prefix
7	
8	law leaf_boolean:
9	  for +key: String
10	  for +position: Nat
11	  for +side: Bool
12	  for route: {Map.bit(key, position) == (key, side) : String & Bool}
13	  {Bool.not(Bool.xor(Inv.bit_value(Map.bit(key, position)), side)) == True{} : Bool}
14	def leaf_boolean(key, position, side, route):
15	  %Equal.sym(String & Bool, Map.bit(key, position), (key, side), route) : {Bool.not(Bool.xor(Inv.bit_value(_), side)) == True{} : Bool}
16	  Equal.cong(Bool, Bool, Bool.not, Bool.xor(side, side), False{}, Prefix.xor_self(side))
17	
18	law routed_boolean:
19	  for -V: Data
20	  for tree: Map<&2, V>
21	  for +position: Nat
22	  for +side: Bool
23	  for route: R.routed(V, tree, position, side)
24	  {Inv.routed(V, tree, position, side) == True{} : Bool}
25	def routed_boolean(V, tree, position, side, route):
26	  match tree:
27	    case MTip{}: {==}
28	    case MLeaf{key, value}: leaf_boolean(key, position, side, route)
29	    case MNode{p, +lo, +hi}:
30	      (left, right) = route
31	      P.conjunction(Inv.routed(V, lo, position, side), Inv.routed(V, hi, position, side), routed_boolean(V, lo, position, side, left), routed_boolean(V, hi, position, side, right))
32	
33	law deletion_preserves:
34	  for -V: Data
35	  for +tree: Map<&2, V>
36	  for +key: String
37	  for +position: Nat
38	  for +side: Bool
39	  for route: {Inv.routed(V, tree, position, side) == True{} : Bool}
40	  {Inv.routed(V, Map.del(&2, V, tree, key), position, side) == True{} : Bool}
41	def deletion_preserves(V, tree, key, position, side, route):
42	  routed_boolean(V, Map.del(&2, V, tree, key), position, side, D.preserves_routing(V, tree, key, position, side, R.routed_certificate(V, tree, position, side, route)))