1	import Base
2	import ./map_routing.bend as Logic
3	import ./string_compare.bend as N
4	
5	# Existing Base.divmod quotient translation; no replacement division algorithm.
6	def next_quotient(pair: Nat & Nat) -> Nat & Nat:
7	  (q, r) = pair
8	  (1n+q, r)
9	
10	law quotient_translation:
11	  for n: Nat
12	  for m: Nat
13	  for +q: Nat
14	  for r: Nat
15	  {Nat.divmod.go(n, m, 1n+q, r) == next_quotient(Nat.divmod.go(n, m, q, r)) : Nat & Nat}
16	def quotient_translation(n, m, q, r):
17	  match n:
18	    case 0n: {==}
19	    case 1n+p:
20	      match m:
21	        case 0n:
22	          quotient_translation(p, r, 1n+q, 0n)
23	        case 1n+k:
24	          quotient_translation(p, k, q, 1n+r)
25	
26	law character_stride:
27	  for position: Nat
28	  {Nat.divmod(Nat.add(33n, position), 33n) == next_quotient(Nat.divmod(position, 33n)) : Nat & Nat}
29	def character_stride(position):
30	  quotient_translation(position, 32n, 0n, 0n)
31	
32	law bit_at_next:
33	  for h: Char
34	  for tail: String
35	  for pair: Nat & Nat
36	  {Map.bit.at(SCon{h, tail}, next_quotient(pair)) == Map.bit.go.rec(h, Map.bit.at(tail, pair)) : String & Bool}
37	def bit_at_next(h, tail, pair):
38	  match pair:
39	    case Tuple{q, r}: {==}
40	
41	# This exact key-preserving result connects bit positions across String prefixes
42	# using the native division and bit traversal definitions.
43	law native_character_stride:
44	  for +h: Char
45	  for +tail: String
46	  for +position: Nat
47	  {Map.bit(SCon{h, tail}, Nat.add(33n, position)) == Map.bit.go.rec(h, Map.bit(tail, position)) : String & Bool}
48	def native_character_stride(h, tail, position):
49	  Equal.trans(String & Bool, Map.bit(SCon{h, tail}, Nat.add(33n, position)), Map.bit.at(SCon{h, tail}, next_quotient(Nat.divmod(position, 33n))), Map.bit.go.rec(h, Map.bit(tail, position)), Equal.cong(Nat & Nat, String & Bool, qr => Map.bit.at(SCon{h, tail}, qr), Nat.divmod(Nat.add(33n, position), 33n), next_quotient(Nat.divmod(position, 33n)), character_stride(position)), bit_at_next(h, tail, Nat.divmod(position, 33n)))
50	
51	law add_right_successor:
52	  for a: Nat
53	  for +b: Nat
54	  {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}
55	def add_right_successor(a, b):
56	  match a:
57	    case 0n: {==}
58	    case 1n+ +p:
59	      Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 1n+b), 1n+Nat.add(p, b), add_right_successor(p, b))
60	
61	law division_no_wrap:
62	  for n: Nat
63	  for m: Nat
64	  for +q: Nat
65	  for +r: Nat
66	  for bound: {Nat.is_le(n, m) == True{} : Bool}
67	  {Nat.divmod.go(n, m, q, r) == (q, Nat.add(n, r)) : Nat & Nat}
68	def division_no_wrap(n, m, q, r, bound):
69	  match n:
70	    case 0n: {==}
71	    case 1n+ +p:
72	      match m:
73	        case 0n:
74	          Empty.absurd({Nat.divmod.go(1n+p, 0n, q, r) == (q, Nat.add(1n+p, r)) : Nat & Nat}, Logic.false_true(bound))
75	        case 1n+ +k:
76	          Equal.trans(Nat & Nat, Nat.divmod.go(p, k, q, 1n+r), (q, Nat.add(p, 1n+r)), (q, 1n+Nat.add(p, r)), division_no_wrap(p, k, q, 1n+r, bound), Equal.cong(Nat, Nat & Nat, s => (q, s), Nat.add(p, 1n+r), 1n+Nat.add(p, r), add_right_successor(p, r)))
77	
78	law first_character_division:
79	  for +position: Nat
80	  for bound: {Nat.is_le(position, 32n) == True{} : Bool}
81	  {Nat.divmod(position, 33n) == (0n, position) : Nat & Nat}
82	def first_character_division(position, bound):
83	  Equal.trans(Nat & Nat, Nat.divmod(position, 33n), (0n, Nat.add(position, 0n)), (0n, position), division_no_wrap(position, 32n, 0n, 0n, bound), Equal.cong(Nat, Nat & Nat, r => (0n, r), Nat.add(position, 0n), position, N.natural_add_right_zero(position)))
84	
85	law native_first_character:
86	  for +head: Char
87	  for +tail: String
88	  for +position: Nat
89	  for bound: {Nat.is_le(position, 32n) == True{} : Bool}
90	  {Map.bit(SCon{head, tail}, position) == Map.bit.go.chr(tail, Map.bit.chr(head, position)) : String & Bool}
91	def native_first_character(head, tail, position, bound):
92	  Equal.cong(Nat & Nat, String & Bool, qr => Map.bit.at(SCon{head, tail}, qr), Nat.divmod(position, 33n), (0n, position), first_character_division(position, bound))