1	import Base
2	
3	def digit(bit: Bool,n: Nat) -> Nat:
4	  match bit:
5	    case False{}:
6	      Nat.double(n)
7	    case True{}:
8	      1n+Nat.double(n)
9	
10	law digits:
11	  for +a: Nat
12	  for +b: Nat
13	  for +ab: Bool
14	  for +bb: Bool
15	  {Nat.cmp(digit(ab,a),digit(bb,b)) == Word.cmp.fin(ab,bb,Nat.cmp(a,b)) : Cmp}
16	def digits(a,b,ab,bb):
17	  match a b ab bb:
18	    case 0n 0n False{} False{}:
19	      {==}
20	    case 0n 0n False{} True{}:
21	      {==}
22	    case 0n 0n True{} False{}:
23	      {==}
24	    case 0n 0n True{} True{}:
25	      {==}
26	    case 0n 1n+bp False{} False{}:
27	      {==}
28	    case 0n 1n+bp False{} True{}:
29	      {==}
30	    case 0n 1n+bp True{} False{}:
31	      {==}
32	    case 0n 1n+bp True{} True{}:
33	      {==}
34	    case 1n+ap 0n False{} False{}:
35	      {==}
36	    case 1n+ap 0n False{} True{}:
37	      {==}
38	    case 1n+ap 0n True{} False{}:
39	      {==}
40	    case 1n+ap 0n True{} True{}:
41	      {==}
42	    case 1n+ap 1n+bp False{} False{}:
43	      digits(ap,bp,False{},False{})
44	    case 1n+ap 1n+bp False{} True{}:
45	      digits(ap,bp,False{},True{})
46	    case 1n+ap 1n+bp True{} False{}:
47	      digits(ap,bp,True{},False{})
48	    case 1n+ap 1n+bp True{} True{}:
49	      digits(ap,bp,True{},True{})
50	
51	law word:
52	  for +n: Nat
53	  for +a: Word(n)
54	  for +b: Word(n)
55	  {Word.cmp(n,a,b) == Nat.cmp(Word.to_nat(n,a),Word.to_nat(n,b)) : Cmp}
56	def word(n,a,b):
57	  match n:
58	    case 0n:
59	      {==}
60	    case 1n+ +p:
61	      match a b:
62	        case WCon{False{},+at} WCon{False{},+bt}:
63	          %Equal.sym(Cmp,Nat.cmp(digit(False{},Word.to_nat(p,at)),digit(False{},Word.to_nat(p,bt))),Word.cmp.fin(False{},False{},
64	              Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),False{},False{})) : {Word.cmp.fin(False{},
65	              False{},Word.cmp(p,at,bt)) == _ : Cmp}
66	          %word(p,at,bt) : {Word.cmp.fin(False{},False{},Word.cmp(p,at,bt)) == Word.cmp.fin(False{},False{},_) : Cmp}
67	          {==}
68	        case WCon{False{},+at} WCon{True{},+bt}:
69	          %Equal.sym(Cmp,Nat.cmp(digit(False{},Word.to_nat(p,at)),digit(True{},Word.to_nat(p,bt))),Word.cmp.fin(False{},True{},
70	              Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),False{},True{})) : {Word.cmp.fin(False{},
71	              True{},Word.cmp(p,at,bt)) == _ : Cmp}
72	          %word(p,at,bt) : {Word.cmp.fin(False{},True{},Word.cmp(p,at,bt)) == Word.cmp.fin(False{},True{},_) : Cmp}
73	          {==}
74	        case WCon{True{},+at} WCon{False{},+bt}:
75	          %Equal.sym(Cmp,Nat.cmp(digit(True{},Word.to_nat(p,at)),digit(False{},Word.to_nat(p,bt))),Word.cmp.fin(True{},False{},
76	              Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),True{},False{})) : {Word.cmp.fin(True{},
77	              False{},Word.cmp(p,at,bt)) == _ : Cmp}
78	          %word(p,at,bt) : {Word.cmp.fin(True{},False{},Word.cmp(p,at,bt)) == Word.cmp.fin(True{},False{},_) : Cmp}
79	          {==}
80	        case WCon{True{},+at} WCon{True{},+bt}:
81	          %Equal.sym(Cmp,Nat.cmp(digit(True{},Word.to_nat(p,at)),digit(True{},Word.to_nat(p,bt))),Word.cmp.fin(True{},True{},
82	              Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),True{},True{})) : {Word.cmp.fin(True{},
83	              True{},Word.cmp(p,at,bt)) == _ : Cmp}
84	          %word(p,at,bt) : {Word.cmp.fin(True{},True{},Word.cmp(p,at,bt)) == Word.cmp.fin(True{},True{},_) : Cmp}
85	          {==}
86	
87	law uint:
88	  for +a: U32
89	  for +b: U32
90	  {U32.cmp(a,b) == Nat.cmp(U32.to_nat(a),U32.to_nat(b)) : Cmp}
91	def uint(a,b):
92	  match a b:
93	    case U32{x} U32{y}:
94	      word(32n,x,y)
95	
96	def lt(+a: U32,+b: U32) -> {U32.is_lt(a,b) == Nat.is_lt(U32.to_nat(a),U32.to_nat(b)) : Bool}:
97	  %uint(a,b) : {Cmp.is_lt(U32.cmp(a,b)) == Cmp.is_lt(_) : Bool}
98	  {==}
99	
100	def le(+a: U32,+b: U32) -> {U32.is_le(a,b) == Nat.is_le(U32.to_nat(a),U32.to_nat(b)) : Bool}:
101	  %uint(a,b) : {Cmp.is_le(U32.cmp(a,b)) == Cmp.is_le(_) : Bool}
102	  {==}
103	
104	def eq(+a: U32,+b: U32) -> {U32.is_eq(a,b) == Nat.is_eq(U32.to_nat(a),U32.to_nat(b)) : Bool}:
105	  %uint(a,b) : {Cmp.is_eq(U32.cmp(a,b)) == Cmp.is_eq(_) : Bool}
106	  {==}
107	
108	def ge(+a: U32,+b: U32) -> {U32.is_ge(a,b) == Nat.is_ge(U32.to_nat(a),U32.to_nat(b)) : Bool}:
109	  %uint(a,b) : {Cmp.is_ge(U32.cmp(a,b)) == Cmp.is_ge(_) : Bool}
110	  {==}