1	# Bendquest verified kernel. Every original gameplay claim is proved below.
2	# No unsafe definitions, axioms, or unfinished proofs.
3	import Base
4	
5	law Bq.Bag:
6	  Data
7	
8	def Bq.Bag():
9	  List<&2, Nat>
10	
11	law Bq.Maybe:
12	  (@-A_0: Data -> Data)
13	
14	def Bq.Maybe(A_0):
15	  Result<&2, &2, Unit, A_0>
16	
17	type Bq.Hero is Data:
18	  Bq.Hero.Hero{inv_0: Bq.Bag, wea_1: Bq.Maybe(Nat), arm_2: Bq.Maybe(Nat), hel_3: Bq.Maybe(Nat), chm_4: Bq.Maybe(Nat), gold_5: Nat, lv_6: Nat, str_7: Nat, agi_8: Nat, vit_9: Nat, pts_10: Nat}
19	
20	law Bq.hero_gold:
21	  (@+h_0: Bq.Hero -> Nat)
22	
23	def Bq.hero_gold(h_0):
24	  match h_0:
25	    case Bq.Hero.Hero{field_1, field_2, field_3, field_4, field_5, field_6, field_7, field_8, field_9, field_10, field_11}:
26	      field_6
27	
28	law Bq.one:
29	  (@+k_0: Nat -> Bq.Bag)
30	
31	def Bq.one(k_0):
32	  match k_0:
33	    case Zero{}:
34	      [1n]
35	    case Succ{field_12}:
36	      Con{0n, Bq.one(field_12)}
37	
38	type Bq.ISlot is Data:
39	  Bq.ISlot.SlotW{}
40	  Bq.ISlot.SlotA{}
41	  Bq.ISlot.SlotH{}
42	  Bq.ISlot.SlotC{}
43	  Bq.ISlot.SlotNone{}
44	
45	type Bq.Info is Data:
46	  Bq.Info.Info{slot_0: Bq.ISlot, lvreq_1: Nat, streq_2: Nat, agireq_3: Nat, vitreq_4: Nat, atk_5: Nat, df_6: Nat, price_7: Nat}
47	
48	law Bq.info_potion:
49	  Bq.Info
50	
51	def Bq.info_potion():
52	  Bq.Info.Info{Bq.ISlot.SlotNone{}, 0n, 0n, 0n, 0n, 0n, 0n, 8n}
53	
54	law Bq.info_weapon:
55	  (@+k_0: Nat -> Bq.Info)
56	
57	def Bq.info_weapon(k_0):
58	  match k_0:
59	    case Zero{}:
60	      Bq.Info.Info{Bq.ISlot.SlotW{}, 1n, 0n, 0n, 0n, 3n, 0n, 12n}
61	    case Succ{field_13}:
62	      match field_13:
63	        case Zero{}:
64	          Bq.Info.Info{Bq.ISlot.SlotW{}, 3n, 4n, 0n, 0n, 6n, 0n, 40n}
65	        case Succ{field_14}:
66	          match field_14:
67	            case Zero{}:
68	              Bq.Info.Info{Bq.ISlot.SlotW{}, 5n, 5n, 3n, 0n, 10n, 0n, 0n}
69	            case Succ{field_15}:
70	              match field_15:
71	                case Zero{}:
72	                  Bq.Info.Info{Bq.ISlot.SlotW{}, 7n, 8n, 0n, 0n, 14n, 0n, 90n}
73	                case Succ{field_16}:
74	                  match field_16:
75	                    case Zero{}:
76	                      Bq.Info.Info{Bq.ISlot.SlotW{}, 10n, 12n, 4n, 0n, 20n, 0n, 0n}
77	                    case Succ{field_17}:
78	                      Bq.Info.Info{Bq.ISlot.SlotW{}, 14n, 16n, 8n, 0n, 30n, 0n, 0n}
79	
80	law Bq.info_armor:
81	  (@+k_0: Nat -> Bq.Info)
82	
83	def Bq.info_armor(k_0):
84	  match k_0:
85	    case Zero{}:
86	      Bq.Info.Info{Bq.ISlot.SlotA{}, 1n, 0n, 0n, 0n, 0n, 1n, 10n}
87	    case Succ{field_18}:
88	      match field_18:
89	        case Zero{}:
90	          Bq.Info.Info{Bq.ISlot.SlotA{}, 3n, 0n, 0n, 3n, 0n, 3n, 35n}
91	        case Succ{field_19}:
92	          match field_19:
93	            case Zero{}:
94	              Bq.Info.Info{Bq.ISlot.SlotA{}, 7n, 0n, 0n, 6n, 0n, 6n, 80n}
95	            case Succ{field_20}:
96	              match field_20:
97	                case Zero{}:
98	                  Bq.Info.Info{Bq.ISlot.SlotA{}, 10n, 0n, 3n, 9n, 0n, 9n, 0n}
99	                case Succ{field_21}:
100	                  Bq.Info.Info{Bq.ISlot.SlotA{}, 14n, 0n, 6n, 12n, 0n, 13n, 0n}
101	
102	law Bq.info_helm:
103	  (@+k_0: Nat -> Bq.Info)
104	
105	def Bq.info_helm(k_0):
106	  match k_0:
107	    case Zero{}:
108	      Bq.Info.Info{Bq.ISlot.SlotH{}, 2n, 0n, 0n, 0n, 0n, 1n, 15n}
109	    case Succ{field_22}:
110	      match field_22:
111	        case Zero{}:
112	          Bq.Info.Info{Bq.ISlot.SlotH{}, 6n, 0n, 0n, 5n, 0n, 4n, 0n}
113	        case Succ{field_23}:
114	          Bq.Info.Info{Bq.ISlot.SlotH{}, 12n, 0n, 5n, 8n, 0n, 8n, 0n}
115	
116	law Bq.info_charm:
117	  (@+k_0: Nat -> Bq.Info)
118	
119	def Bq.info_charm(k_0):
120	  match k_0:
121	    case Zero{}:
122	      Bq.Info.Info{Bq.ISlot.SlotC{}, 4n, 0n, 3n, 0n, 0n, 0n, 60n}
123	    case Succ{field_24}:
124	      match field_24:
125	        case Zero{}:
126	          Bq.Info.Info{Bq.ISlot.SlotC{}, 6n, 5n, 0n, 0n, 4n, 0n, 0n}
127	        case Succ{field_25}:
128	          Bq.Info.Info{Bq.ISlot.SlotC{}, 9n, 0n, 0n, 5n, 0n, 2n, 0n}
129	
130	law Bq.Nat.sub:
131	  (@+a_0: Nat -> (@+b_1: Nat -> Nat))
132	
133	def Bq.Nat.sub(a_0, b_1):
134	  match a_0:
135	    case Zero{}:
136	      0n
137	    case Succ{field_26}:
138	      match b_1:
139	        case Zero{}:
140	          Succ{field_26}
141	        case Succ{field_27}:
142	          Bq.Nat.sub(field_26, field_27)
143	
144	law Bq.Nat.le:
145	  (@+a_0: Nat -> (@+b_1: Nat -> Bool))
146	
147	def Bq.Nat.le(a_0, b_1):
148	  match a_0:
149	    case Zero{}:
150	      True{}
151	    case Succ{field_28}:
152	      match b_1:
153	        case Zero{}:
154	          False{}
155	        case Succ{field_29}:
156	          Bq.Nat.le(field_28, field_29)
157	
158	law Bq.item_info:
159	  (@+k_0: Nat -> Bq.Info)
160	
161	def Bq.item_info(k_0):
162	  match k_0:
163	    case Zero{}:
164	      Bq.info_potion
165	    case Succ{field_30}:
166	      (apply_1 = {(p_0 => \{True: Bq.info_weapon(p_0); \{False: (apply_2 = {(p_0 => \{True: Bq.info_armor(Bq.Nat.sub(p_0, 6n)); \{False: (apply_3 = {(p_0 => \{True: Bq.info_helm(Bq.Nat.sub(p_0, 11n)); \{False: (apply_4 = {(p_0 => \{True: Bq.info_charm(Bq.Nat.sub(p_0, 14n)); \{False: Bq.Info.Info{Bq.ISlot.SlotNone{}, 0n, 0n, 0n, 0n, 0n, 0n, 0n}; \{}}}) : (@+p_0: Nat -> (@+___1: Bool -> Bq.Info))}; apply_4(p_0, Bq.Nat.le(p_0, 16n))); \{}}}) : (@+p_0: Nat -> (@+___1: Bool -> Bq.Info))}; apply_3(p_0, Bq.Nat.le(p_0, 13n))); \{}}}) : (@+p_0: Nat -> (@+___1: Bool -> Bq.Info))}; apply_2(p_0, Bq.Nat.le(p_0, 10n))); \{}}}) : (@+p_0: Nat -> (@+___1: Bool -> Bq.Info))}; apply_1(field_30, Bq.Nat.le(field_30, 5n)))
167	
168	law Bq.islot:
169	  (@+k_0: Nat -> Bq.ISlot)
170	
171	def Bq.islot(k_0):
172	  (apply_5 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => slot_0)))))))); \{}} : (@+___0: Bq.Info -> Bq.ISlot)}; apply_5(Bq.item_info(k_0)))
173	
174	law Bq.Bag.sub:
175	  (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> Bq.Bag))
176	
177	def Bq.Bag.sub(a_0, b_1):
178	  match a_0:
179	    case Con{field_31, field_32}:
180	      match b_1:
181	        case Con{field_33, field_34}:
182	          Con{Bq.Nat.sub(field_31, field_33), Bq.Bag.sub(field_32, field_34)}
183	        case Nil{}:
184	          Con{field_31, field_32}
185	    case Nil{}:
186	      Nil{}
187	
188	law Bq.Maybe.some:
189	  (@-A_0: Data -> (@+value_1: A_0 -> Bq.Maybe(A_0)))
190	
191	def Bq.Maybe.some(A_0, value_1):
192	  Done{value_1}
193	
194	law Bq.do_equip:
195	  (@+k_0: Nat -> (@+h_1: Bq.Hero -> Bq.Hero))
196	
197	def Bq.do_equip(k_0, h_1):
198	  match h_1:
199	    case Bq.Hero.Hero{field_35, field_36, field_37, field_38, field_39, field_40, field_41, field_42, field_43, field_44, field_45}:
200	      (apply_6 = {(inv_0 => (k_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => (wea_11 => \{Bq.ISlot.SlotW: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), Bq.Maybe.some(Nat, k_1), arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotA: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), wea_11, Bq.Maybe.some(Nat, k_1), hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotH: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), wea_11, arm_2, Bq.Maybe.some(Nat, k_1), chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotC: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), wea_11, arm_2, hel_3, Bq.Maybe.some(Nat, k_1), gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotNone: Bq.Hero.Hero{inv_0, wea_11, arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{}}}}}})))))))))))) : (@+inv_0: Bq.Bag -> (@+k_1: Nat -> (@+arm_2: Bq.Maybe(Nat) -> (@+hel_3: Bq.Maybe(Nat) -> (@+chm_4: Bq.Maybe(Nat) -> (@+gold_5: Nat -> (@+lv_6: Nat -> (@+str_7: Nat -> (@+agi_8: Nat -> (@+vit_9: Nat -> (@+pts_10: Nat -> (@+wea_11: Bq.Maybe(Nat) -> (@+___12: Bq.ISlot -> Bq.Hero)))))))))))))}; apply_6(field_35, k_0, field_37, field_38, field_39, field_40, field_41, field_42, field_43, field_44, field_45, field_36, Bq.islot(k_0)))
201	
202	law Bq.mb:
203	  (@+m_0: Bq.Maybe(Nat) -> Bq.Bag)
204	
205	def Bq.mb(m_0):
206	  match m_0:
207	    case Done{field_46}:
208	      Bq.one(field_46)
209	    case Fail{field_47}:
210	      Nil{}
211	
212	law Bq.Nat.add:
213	  (@+a_0: Nat -> (@+b_1: Nat -> Nat))
214	
215	def Bq.Nat.add(a_0, b_1):
216	  match a_0:
217	    case Zero{}:
218	      b_1
219	    case Succ{field_48}:
220	      Succ{Bq.Nat.add(field_48, b_1)}
221	
222	law Bq.Bag.add:
223	  (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> Bq.Bag))
224	
225	def Bq.Bag.add(a_0, b_1):
226	  match a_0:
227	    case Con{field_49, field_50}:
228	      match b_1:
229	        case Con{field_51, field_52}:
230	          Con{Bq.Nat.add(field_49, field_51), Bq.Bag.add(field_50, field_52)}
231	        case Nil{}:
232	          Con{field_49, field_50}
233	    case Nil{}:
234	      b_1
235	
236	law Bq.Maybe.none:
237	  (@-A_0: Data -> Bq.Maybe(A_0))
238	
239	def Bq.Maybe.none(A_0):
240	  Fail{Unit{}}
241	
242	law Bq.do_unequip:
243	  (@+s_0: Bq.ISlot -> (@+h_1: Bq.Hero -> Bq.Hero))
244	
245	def Bq.do_unequip(s_0, h_1):
246	  match h_1:
247	    case Bq.Hero.Hero{field_53, field_54, field_55, field_56, field_57, field_58, field_59, field_60, field_61, field_62, field_63}:
248	      (apply_7 = {\{Bq.ISlot.SlotW: (inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => Bq.Hero.Hero{Bq.Bag.add(Bq.mb(wea_1), inv_0), Bq.Maybe.none(Nat), arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}))))))))))); \{Bq.ISlot.SlotA: (inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => Bq.Hero.Hero{Bq.Bag.add(Bq.mb(arm_2), inv_0), wea_1, Bq.Maybe.none(Nat), hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}))))))))))); \{Bq.ISlot.SlotH: (inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => Bq.Hero.Hero{Bq.Bag.add(Bq.mb(hel_3), inv_0), wea_1, arm_2, Bq.Maybe.none(Nat), chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}))))))))))); \{Bq.ISlot.SlotC: (inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => Bq.Hero.Hero{Bq.Bag.add(Bq.mb(chm_4), inv_0), wea_1, arm_2, hel_3, Bq.Maybe.none(Nat), gold_5, lv_6, str_7, agi_8, vit_9, pts_10}))))))))))); \{Bq.ISlot.SlotNone: (inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => Bq.Hero.Hero{inv_0, wea_1, arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}))))))))))); \{}}}}}} : (@+___0: Bq.ISlot -> (@+__1: List<&2, Nat> -> (@+__2: Result<&2, &2, Unit, Nat> -> (@+__3: Result<&2, &2, Unit, Nat> -> (@+__4: Result<&2, &2, Unit, Nat> -> (@+__5: Result<&2, &2, Unit, Nat> -> (@+__6: Nat -> (@+__7: Nat -> (@+__8: Nat -> (@+__9: Nat -> (@+__10: Nat -> (@+__11: Nat -> Bq.Hero))))))))))))}; apply_7(s_0, field_53, field_54, field_55, field_56, field_57, field_58, field_59, field_60, field_61, field_62, field_63))
249	
250	law Bq.iprice:
251	  (@+k_0: Nat -> Nat)
252	
253	def Bq.iprice(k_0):
254	  (apply_8 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => price_7)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_8(Bq.item_info(k_0)))
255	
256	law Bq.do_buy:
257	  (@+k_0: Nat -> (@+h_1: Bq.Hero -> Bq.Hero))
258	
259	def Bq.do_buy(k_0, h_1):
260	  match h_1:
261	    case Bq.Hero.Hero{field_64, field_65, field_66, field_67, field_68, field_69, field_70, field_71, field_72, field_73, field_74}:
262	      Bq.Hero.Hero{Bq.Bag.add(Bq.one(k_0), field_64), field_65, field_66, field_67, field_68, Bq.Nat.sub(field_69, Bq.iprice(k_0)), field_70, field_71, field_72, field_73, field_74}
263	
264	law Bq.POTION:
265	  Nat
266	
267	def Bq.POTION():
268	  0n
269	
270	law Bq.do_quaff:
271	  (@+h_0: Bq.Hero -> Bq.Hero)
272	
273	def Bq.do_quaff(h_0):
274	  match h_0:
275	    case Bq.Hero.Hero{field_75, field_76, field_77, field_78, field_79, field_80, field_81, field_82, field_83, field_84, field_85}:
276	      Bq.Hero.Hero{Bq.Bag.sub(field_75, Bq.one(Bq.POTION)), field_76, field_77, field_78, field_79, field_80, field_81, field_82, field_83, field_84, field_85}
277	
278	law Bq.do_alloc:
279	  (@+s_0: Nat -> (@+h_1: Bq.Hero -> Bq.Hero))
280	
281	def Bq.do_alloc(s_0, h_1):
282	  match h_1:
283	    case Bq.Hero.Hero{field_86, field_87, field_88, field_89, field_90, field_91, field_92, field_93, field_94, field_95, field_96}:
284	      match field_96:
285	        case Zero{}:
286	          Bq.Hero.Hero{field_86, field_87, field_88, field_89, field_90, field_91, field_92, field_93, field_94, field_95, 0n}
287	        case Succ{field_97}:
288	          (apply_9 = {(inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => \{Zero: (p_10 => Bq.Hero.Hero{inv_0, wea_1, arm_2, hel_3, chm_4, gold_5, lv_6, Succ{str_7}, agi_8, vit_9, p_10}); \{Succ: (p_10 => (apply_10 = {(inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => \{Zero: (p_10 => Bq.Hero.Hero{inv_0, wea_1, arm_2, hel_3, chm_4, gold_5, lv_6, str_7, Succ{agi_8}, vit_9, p_10}); \{Succ: (p_10 => (p_11 => Bq.Hero.Hero{inv_0, wea_1, arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, Succ{vit_9}, p_11})); \{}}})))))))))) : (@+inv_0: Bq.Bag -> (@+wea_1: Bq.Maybe(Nat) -> (@+arm_2: Bq.Maybe(Nat) -> (@+hel_3: Bq.Maybe(Nat) -> (@+chm_4: Bq.Maybe(Nat) -> (@+gold_5: Nat -> (@+lv_6: Nat -> (@+str_7: Nat -> (@+agi_8: Nat -> (@+vit_9: Nat -> (@+___10: Nat -> (@+__11: Nat -> Bq.Hero))))))))))))}; apply_10(inv_0, wea_1, arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, p_10))); \{}}})))))))))) : (@+inv_0: Bq.Bag -> (@+wea_1: Bq.Maybe(Nat) -> (@+arm_2: Bq.Maybe(Nat) -> (@+hel_3: Bq.Maybe(Nat) -> (@+chm_4: Bq.Maybe(Nat) -> (@+gold_5: Nat -> (@+lv_6: Nat -> (@+str_7: Nat -> (@+agi_8: Nat -> (@+vit_9: Nat -> (@+___10: Nat -> (@+__11: Nat -> Bq.Hero))))))))))))}; apply_9(field_86, field_87, field_88, field_89, field_90, field_91, field_92, field_93, field_94, field_95, s_0, field_97))
289	
290	law Bq.do_levelup:
291	  (@+h_0: Bq.Hero -> Bq.Hero)
292	
293	def Bq.do_levelup(h_0):
294	  match h_0:
295	    case Bq.Hero.Hero{field_98, field_99, field_100, field_101, field_102, field_103, field_104, field_105, field_106, field_107, field_108}:
296	      Bq.Hero.Hero{field_98, field_99, field_100, field_101, field_102, field_103, Succ{field_104}, field_105, field_106, field_107, Bq.Nat.add(3n, field_108)}
297	
298	type Bq.HOp is Data:
299	  Bq.HOp.Equip{k_0: Nat}
300	  Bq.HOp.Unequip{s_0: Bq.ISlot}
301	  Bq.HOp.Buy{k_0: Nat}
302	  Bq.HOp.Quaff{}
303	  Bq.HOp.Alloc{s_0: Nat}
304	  Bq.HOp.LevelUp{}
305	
306	law Bq.hop_do:
307	  (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> Bq.Hero))
308	
309	def Bq.hop_do(op_0, h_1):
310	  match op_0:
311	    case Bq.HOp.Equip{field_109}:
312	      Bq.do_equip(field_109, h_1)
313	    case Bq.HOp.Unequip{field_110}:
314	      Bq.do_unequip(field_110, h_1)
315	    case Bq.HOp.Buy{field_111}:
316	      Bq.do_buy(field_111, h_1)
317	    case Bq.HOp.Quaff{}:
318	      Bq.do_quaff(h_1)
319	    case Bq.HOp.Alloc{field_112}:
320	      Bq.do_alloc(field_112, h_1)
321	    case Bq.HOp.LevelUp{}:
322	      Bq.do_levelup(h_1)
323	
324	law Bq.hero_step_go:
325	  (@+v_0: Bool -> (@+op_1: Bq.HOp -> (@+h_2: Bq.Hero -> Bq.Hero)))
326	
327	def Bq.hero_step_go(v_0, op_1, h_2):
328	  match v_0:
329	    case True{}:
330	      Bq.hop_do(op_1, h_2)
331	    case False{}:
332	      h_2
333	
334	law Bq.slot_empty:
335	  (@+m_0: Bq.Maybe(Nat) -> Bool)
336	
337	def Bq.slot_empty(m_0):
338	  match m_0:
339	    case Done{field_113}:
340	      False{}
341	    case Fail{field_114}:
342	      True{}
343	
344	law Bq.ilvreq:
345	  (@+k_0: Nat -> Nat)
346	
347	def Bq.ilvreq(k_0):
348	  (apply_11 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => lvreq_1)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_11(Bq.item_info(k_0)))
349	
350	law Bq.istreq:
351	  (@+k_0: Nat -> Nat)
352	
353	def Bq.istreq(k_0):
354	  (apply_12 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => streq_2)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_12(Bq.item_info(k_0)))
355	
356	law Bq.iagireq:
357	  (@+k_0: Nat -> Nat)
358	
359	def Bq.iagireq(k_0):
360	  (apply_13 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => agireq_3)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_13(Bq.item_info(k_0)))
361	
362	law Bq.ivitreq:
363	  (@+k_0: Nat -> Nat)
364	
365	def Bq.ivitreq(k_0):
366	  (apply_14 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => vitreq_4)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_14(Bq.item_info(k_0)))
367	
368	law Bq.Bool.and:
369	  (@+a_0: Bool -> (@+b_1: Bool -> Bool))
370	
371	def Bq.Bool.and(a_0, b_1):
372	  match a_0:
373	    case True{}:
374	      b_1
375	    case False{}:
376	      False{}
377	
378	law Bq.can_wear:
379	  (@+k_0: Nat -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> Bool)))))
380	
381	def Bq.can_wear(k_0, lv_1, str_2, agi_3, vit_4):
382	  Bq.Bool.and(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))))
383	
384	law Bq.Bag.le:
385	  (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> Bool))
386	
387	def Bq.Bag.le(a_0, b_1):
388	  match a_0:
389	    case Con{field_115, field_116}:
390	      match b_1:
391	        case Con{field_117, field_118}:
392	          Bq.Bool.and(Bq.Nat.le(field_115, field_117), Bq.Bag.le(field_116, field_118))
393	        case Nil{}:
394	          False{}
395	    case Nil{}:
396	      True{}
397	
398	law Bq.equip_ok:
399	  (@+k_0: Nat -> (@+h_1: Bq.Hero -> Bool))
400	
401	def Bq.equip_ok(k_0, h_1):
402	  (apply_15 = {(k_0 => (h_1 => \{Bq.ISlot.SlotNone: False{}; \{Bq.ISlot.SlotW: (apply_16 = {(k_0 => \{Bq.Hero.Hero: (inv_1 => (wea_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => Bq.Bool.and(Bq.Bag.le(Bq.one(k_0), inv_1), Bq.Bool.and(Bq.slot_empty(wea_2), Bq.can_wear(k_0, lv_7, str_8, agi_9, vit_10)))))))))))))); \{}}) : (@+k_0: Nat -> (@+___1: Bq.Hero -> Bool))}; apply_16(k_0, h_1)); \{Bq.ISlot.SlotA: (apply_17 = {(k_0 => \{Bq.Hero.Hero: (inv_1 => (wea_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => Bq.Bool.and(Bq.Bag.le(Bq.one(k_0), inv_1), Bq.Bool.and(Bq.slot_empty(arm_3), Bq.can_wear(k_0, lv_7, str_8, agi_9, vit_10)))))))))))))); \{}}) : (@+k_0: Nat -> (@+___1: Bq.Hero -> Bool))}; apply_17(k_0, h_1)); \{Bq.ISlot.SlotH: (apply_18 = {(k_0 => \{Bq.Hero.Hero: (inv_1 => (wea_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => Bq.Bool.and(Bq.Bag.le(Bq.one(k_0), inv_1), Bq.Bool.and(Bq.slot_empty(hel_4), Bq.can_wear(k_0, lv_7, str_8, agi_9, vit_10)))))))))))))); \{}}) : (@+k_0: Nat -> (@+___1: Bq.Hero -> Bool))}; apply_18(k_0, h_1)); \{Bq.ISlot.SlotC: (apply_19 = {(k_0 => \{Bq.Hero.Hero: (inv_1 => (wea_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => Bq.Bool.and(Bq.Bag.le(Bq.one(k_0), inv_1), Bq.Bool.and(Bq.slot_empty(chm_5), Bq.can_wear(k_0, lv_7, str_8, agi_9, vit_10)))))))))))))); \{}}) : (@+k_0: Nat -> (@+___1: Bq.Hero -> Bool))}; apply_19(k_0, h_1)); \{}}}}}})) : (@+k_0: Nat -> (@+h_1: Bq.Hero -> (@+___2: Bq.ISlot -> Bool)))}; apply_15(k_0, h_1, Bq.islot(k_0)))
403	
404	law Bq.slot_of:
405	  (@+h_0: Bq.Hero -> (@+s_1: Bq.ISlot -> Bq.Maybe(Nat)))
406	
407	def Bq.slot_of(h_0, s_1):
408	  match h_0:
409	    case Bq.Hero.Hero{field_119, field_120, field_121, field_122, field_123, field_124, field_125, field_126, field_127, field_128, field_129}:
410	      match s_1:
411	        case Bq.ISlot.SlotW{}:
412	          field_120
413	        case Bq.ISlot.SlotA{}:
414	          field_121
415	        case Bq.ISlot.SlotH{}:
416	          field_122
417	        case Bq.ISlot.SlotC{}:
418	          field_123
419	        case Bq.ISlot.SlotNone{}:
420	          Bq.Maybe.none(Nat)
421	
422	law Bq.Bool.not:
423	  (@+a_0: Bool -> Bool)
424	
425	def Bq.Bool.not(a_0):
426	  match a_0:
427	    case True{}:
428	      False{}
429	    case False{}:
430	      True{}
431	
432	law Bq.unequip_ok:
433	  (@+s_0: Bq.ISlot -> (@+h_1: Bq.Hero -> Bool))
434	
435	def Bq.unequip_ok(s_0, h_1):
436	  Bq.Bool.not(Bq.slot_empty(Bq.slot_of(h_1, s_0)))
437	
438	law Bq.Nat.lt:
439	  (@+a_0: Nat -> (@+b_1: Nat -> Bool))
440	
441	def Bq.Nat.lt(a_0, b_1):
442	  Bq.Nat.le(Succ{a_0}, b_1)
443	
444	law Bq.buy_ok:
445	  (@+k_0: Nat -> (@+h_1: Bq.Hero -> Bool))
446	
447	def Bq.buy_ok(k_0, h_1):
448	  Bq.Bool.and(Bq.Nat.lt(0n, Bq.iprice(k_0)), Bq.Nat.le(Bq.iprice(k_0), Bq.hero_gold(h_1)))
449	
450	law Bq.quaff_ok:
451	  (@+h_0: Bq.Hero -> Bool)
452	
453	def Bq.quaff_ok(h_0):
454	  match h_0:
455	    case Bq.Hero.Hero{field_130, field_131, field_132, field_133, field_134, field_135, field_136, field_137, field_138, field_139, field_140}:
456	      Bq.Bag.le(Bq.one(Bq.POTION), field_130)
457	
458	law Bq.alloc_ok:
459	  (@+h_0: Bq.Hero -> Bool)
460	
461	def Bq.alloc_ok(h_0):
462	  match h_0:
463	    case Bq.Hero.Hero{field_141, field_142, field_143, field_144, field_145, field_146, field_147, field_148, field_149, field_150, field_151}:
464	      Bq.Nat.lt(0n, field_151)
465	
466	law Bq.hop_ok:
467	  (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> Bool))
468	
469	def Bq.hop_ok(op_0, h_1):
470	  match op_0:
471	    case Bq.HOp.Equip{field_152}:
472	      Bq.equip_ok(field_152, h_1)
473	    case Bq.HOp.Unequip{field_153}:
474	      Bq.unequip_ok(field_153, h_1)
475	    case Bq.HOp.Buy{field_154}:
476	      Bq.buy_ok(field_154, h_1)
477	    case Bq.HOp.Quaff{}:
478	      Bq.quaff_ok(h_1)
479	    case Bq.HOp.Alloc{field_155}:
480	      Bq.alloc_ok(h_1)
481	    case Bq.HOp.LevelUp{}:
482	      True{}
483	
484	law Bq.hero_step:
485	  (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> Bq.Hero))
486	
487	def Bq.hero_step(op_0, h_1):
488	  Bq.hero_step_go(Bq.hop_ok(op_0, h_1), op_0, h_1)
489	
490	law Bq.Nat.mul:
491	  (@+a_0: Nat -> (@+b_1: Nat -> Nat))
492	
493	def Bq.Nat.mul(a_0, b_1):
494	  match a_0:
495	    case Zero{}:
496	      0n
497	    case Succ{field_156}:
498	      Bq.Nat.add(b_1, Bq.Nat.mul(field_156, b_1))
499	
500	law Bq.Nat.dbl:
501	  (@+n_0: Nat -> Nat)
502	
503	def Bq.Nat.dbl(n_0):
504	  match n_0:
505	    case Zero{}:
506	      0n
507	    case Succ{field_157}:
508	      Succ{Succ{Bq.Nat.dbl(field_157)}}
509	
510	law Bq.Nat.pred:
511	  (@+n_0: Nat -> Nat)
512	
513	def Bq.Nat.pred(n_0):
514	  match n_0:
515	    case Zero{}:
516	      0n
517	    case Succ{field_158}:
518	      field_158
519	
520	law Bq.max_hp:
521	  (@+lv_0: Nat -> (@+vit_1: Nat -> Nat))
522	
523	def Bq.max_hp(lv_0, vit_1):
524	  Bq.Nat.add(20n, Bq.Nat.add(Bq.Nat.mul(5n, vit_1), Bq.Nat.dbl(Bq.Nat.pred(lv_0))))
525	
526	law Bq.crit_dbl:
527	  (@+crit_0: Bool -> (@+raw_1: Nat -> Nat))
528	
529	def Bq.crit_dbl(crit_0, raw_1):
530	  match crit_0:
531	    case True{}:
532	      Bq.Nat.dbl(raw_1)
533	    case False{}:
534	      raw_1
535	
536	law Bq.nmin:
537	  (@+a_0: Nat -> (@+b_1: Nat -> Nat))
538	
539	def Bq.nmin(a_0, b_1):
540	  match a_0:
541	    case Zero{}:
542	      0n
543	    case Succ{field_159}:
544	      match b_1:
545	        case Zero{}:
546	          0n
547	        case Succ{field_160}:
548	          Succ{Bq.nmin(field_159, field_160)}
549	
550	law Bq.nmax:
551	  (@+a_0: Nat -> (@+b_1: Nat -> Nat))
552	
553	def Bq.nmax(a_0, b_1):
554	  match a_0:
555	    case Zero{}:
556	      b_1
557	    case Succ{field_161}:
558	      match b_1:
559	        case Zero{}:
560	          Succ{field_161}
561	        case Succ{field_162}:
562	          Succ{Bq.nmax(field_161, field_162)}
563	
564	law Bq.DMG_CAP:
565	  Nat
566	
567	def Bq.DMG_CAP():
568	  999n
569	
570	law Bq.damage:
571	  (@+watk_0: Nat -> (@+str_1: Nat -> (@+df_2: Nat -> (@+crit_3: Bool -> Nat))))
572	
573	def Bq.damage(watk_0, str_1, df_2, crit_3):
574	  (+raw2_4 = Bq.crit_dbl(crit_3, Bq.Nat.add(watk_0, Bq.Nat.dbl(str_1))); Bq.nmin(Bq.nmax(Bq.Nat.sub(raw2_4, df_2), 1n), Bq.DMG_CAP))
575	
576	law Bq.iatk:
577	  (@+k_0: Nat -> Nat)
578	
579	def Bq.iatk(k_0):
580	  (apply_20 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => atk_5)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_20(Bq.item_info(k_0)))
581	
582	law Bq.fresh_hero:
583	  Bq.Hero
584	
585	def Bq.fresh_hero():
586	  Bq.Hero.Hero{Nil{}, Bq.Maybe.none(Nat), Bq.Maybe.none(Nat), Bq.Maybe.none(Nat), Bq.Maybe.none(Nat), 10n, 1n, 3n, 3n, 3n, 0n}
587	
588	law Bq.idf:
589	  (@+k_0: Nat -> Nat)
590	
591	def Bq.idf(k_0):
592	  (apply_21 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => df_6)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_21(Bq.item_info(k_0)))
593	
594	law Bq.mob_damage:
595	  (@+matk_0: Nat -> (@+df_1: Nat -> (@+maxhp_2: Nat -> Nat)))
596	
597	def Bq.mob_damage(matk_0, df_1, maxhp_2):
598	  Bq.nmax(Bq.nmin(Bq.nmax(Bq.Nat.sub(matk_0, df_1), 1n), Bq.Nat.pred(maxhp_2)), 1n)
599	
600	type Bq.Dir is Data:
601	  Bq.Dir.DU{}
602	  Bq.Dir.DD{}
603	  Bq.Dir.DL{}
604	  Bq.Dir.DR{}
605	
606	law Bq.walk_x:
607	  (@+w_0: Nat -> (@+x_1: Nat -> (@+d_2: Bq.Dir -> Nat)))
608	
609	def Bq.walk_x(w_0, x_1, d_2):
610	  match d_2:
611	    case Bq.Dir.DL{}:
612	      Bq.Nat.pred(x_1)
613	    case Bq.Dir.DR{}:
614	      (apply_22 = {(x_0 => \{True: Succ{x_0}; \{False: x_0; \{}}}) : (@+x_0: Nat -> (@+___1: Bool -> Nat))}; apply_22(x_1, Bq.Nat.lt(Succ{x_1}, w_0)))
615	    case Bq.Dir.DU{}:
616	      x_1
617	    case Bq.Dir.DD{}:
618	      x_1
619	
620	law Bq.walk_y:
621	  (@+h_0: Nat -> (@+y_1: Nat -> (@+d_2: Bq.Dir -> Nat)))
622	
623	def Bq.walk_y(h_0, y_1, d_2):
624	  match d_2:
625	    case Bq.Dir.DU{}:
626	      Bq.Nat.pred(y_1)
627	    case Bq.Dir.DD{}:
628	      (apply_23 = {(y_0 => \{True: Succ{y_0}; \{False: y_0; \{}}}) : (@+y_0: Nat -> (@+___1: Bool -> Nat))}; apply_23(y_1, Bq.Nat.lt(Succ{y_1}, h_0)))
629	    case Bq.Dir.DL{}:
630	      y_1
631	    case Bq.Dir.DR{}:
632	      y_1
633	
634	law Bq.Pair.Pair:
635	  (@-A_0: Data -> (@-B_1: (@-__1: A_0 -> Data) -> Data))
636	
637	def Bq.Pair.Pair(A_0, B_1):
638	  Sigma<&2, &2, A_0, B_1>
639	
640	law Bq.walk:
641	  (@+w_0: Nat -> (@+h_1: Nat -> (@+x_2: Nat -> (@+y_3: Nat -> (@+d_4: Bq.Dir -> Bq.Pair.Pair(Nat, (__5 => Nat)))))))
642	
643	def Bq.walk(w_0, h_1, x_2, y_3, d_4):
644	  Tuple{Bq.walk_x(w_0, x_2, d_4), Bq.walk_y(h_1, y_3, d_4)}
645	
646	law Bq.rejected_op_is_noop:
647	  (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> (@+__2: {Bq.hop_ok(op_0, h_1) == False{} : Bool} -> {Bq.hero_step(op_0, h_1) == h_1 : Bq.Hero})))
648	
649	def Bq.rejected_op_is_noop(op_0, h_1, __2):
650	  (%Equal.sym(Bool, Bq.hop_ok(op_0, h_1), False{}, __2) : {Bq.hero_step_go(_, op_0, h_1) == h_1 : Bq.Hero}; {==})
651	
652	law Bq.gear_bag:
653	  (@+wea_0: Bq.Maybe(Nat) -> (@+arm_1: Bq.Maybe(Nat) -> (@+hel_2: Bq.Maybe(Nat) -> (@+chm_3: Bq.Maybe(Nat) -> Bq.Bag))))
654	
655	def Bq.gear_bag(wea_0, arm_1, hel_2, chm_3):
656	  Bq.Bag.add(Bq.mb(wea_0), Bq.Bag.add(Bq.mb(arm_1), Bq.Bag.add(Bq.mb(hel_2), Bq.mb(chm_3))))
657	
658	law Bq.census:
659	  (@+h_0: Bq.Hero -> Bq.Bag)
660	
661	def Bq.census(h_0):
662	  match h_0:
663	    case Bq.Hero.Hero{field_163, field_164, field_165, field_166, field_167, field_168, field_169, field_170, field_171, field_172, field_173}:
664	      Bq.Bag.add(field_163, Bq.gear_bag(field_164, field_165, field_166, field_167))
665	
666	law Bq.Nat.add_zero:
667	  (@+a_0: Nat -> {Bq.Nat.add(a_0, 0n) == a_0 : Nat})
668	
669	def Bq.Nat.add_zero(a_0):
670	  match a_0:
671	    case Zero{}:
672	      {==}
673	    case Succ{field_174}:
674	      (%Equal.sym(Nat, Bq.Nat.add(field_174, 0n), field_174, Bq.Nat.add_zero(field_174)) : {Succ{_} == Succ{field_174} : Nat}; {==})
675	
676	law Bq.Nat.add_succ:
677	  (@+a_0: Nat -> (@+b_1: Nat -> {Bq.Nat.add(a_0, Succ{b_1}) == Succ{Bq.Nat.add(a_0, b_1)} : Nat}))
678	
679	def Bq.Nat.add_succ(a_0, b_1):
680	  match a_0:
681	    case Zero{}:
682	      {==}
683	    case Succ{field_175}:
684	      (%Equal.sym(Nat, Bq.Nat.add(field_175, Succ{b_1}), Succ{Bq.Nat.add(field_175, b_1)}, Bq.Nat.add_succ(field_175, b_1)) : {Succ{_} == Succ{Succ{Bq.Nat.add(field_175, b_1)}} : Nat}; {==})
685	
686	law Bq.Nat.add_comm:
687	  (@+a_0: Nat -> (@+b_1: Nat -> {Bq.Nat.add(a_0, b_1) == Bq.Nat.add(b_1, a_0) : Nat}))
688	
689	def Bq.Nat.add_comm(a_0, b_1):
690	  match a_0:
691	    case Zero{}:
692	      (%Equal.sym(Nat, Bq.Nat.add(b_1, 0n), b_1, Bq.Nat.add_zero(b_1)) : {b_1 == _ : Nat}; {==})
693	    case Succ{field_176}:
694	      (%Equal.sym(Nat, Bq.Nat.add(b_1, Succ{field_176}), Succ{Bq.Nat.add(b_1, field_176)}, Bq.Nat.add_succ(b_1, field_176)) : {Succ{Bq.Nat.add(field_176, b_1)} == _ : Nat}; (%Equal.sym(Nat, Bq.Nat.add(field_176, b_1), Bq.Nat.add(b_1, field_176), Bq.Nat.add_comm(field_176, b_1)) : {Succ{_} == Succ{Bq.Nat.add(b_1, field_176)} : Nat}; {==}))
695	
696	law Bq.Bag.add_nil:
697	  (@+a_0: Bq.Bag -> {Bq.Bag.add(a_0, Nil{}) == a_0 : Bq.Bag})
698	
699	def Bq.Bag.add_nil(a_0):
700	  match a_0:
701	    case Con{field_177, field_178}:
702	      {==}
703	    case Nil{}:
704	      {==}
705	
706	law Bq.Bag.add_comm:
707	  (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> {Bq.Bag.add(a_0, b_1) == Bq.Bag.add(b_1, a_0) : Bq.Bag}))
708	
709	def Bq.Bag.add_comm(a_0, b_1):
710	  match a_0:
711	    case Con{field_179, field_180}:
712	      match b_1:
713	        case Con{field_181, field_182}:
714	          (%Equal.sym(Nat, Bq.Nat.add(field_179, field_181), Bq.Nat.add(field_181, field_179), Bq.Nat.add_comm(field_179, field_181)) : {Con{_, Bq.Bag.add(field_180, field_182)} == Con{Bq.Nat.add(field_181, field_179), Bq.Bag.add(field_182, field_180)} : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(field_180, field_182), Bq.Bag.add(field_182, field_180), Bq.Bag.add_comm(field_180, field_182)) : {Con{Bq.Nat.add(field_181, field_179), _} == Con{Bq.Nat.add(field_181, field_179), Bq.Bag.add(field_182, field_180)} : List<&2, Nat>}; {==}))
715	        case Nil{}:
716	          {==}
717	    case Nil{}:
718	      (%Equal.sym(Bq.Bag, Bq.Bag.add(b_1, Nil{}), b_1, Bq.Bag.add_nil(b_1)) : {b_1 == _ : List<&2, Nat>}; {==})
719	
720	law Bq.Nat.add_assoc:
721	  (@+a_0: Nat -> (@+b_1: Nat -> (@+c_2: Nat -> {Bq.Nat.add(Bq.Nat.add(a_0, b_1), c_2) == Bq.Nat.add(a_0, Bq.Nat.add(b_1, c_2)) : Nat})))
722	
723	def Bq.Nat.add_assoc(a_0, b_1, c_2):
724	  match a_0:
725	    case Zero{}:
726	      {==}
727	    case Succ{field_183}:
728	      (%Equal.sym(Nat, Bq.Nat.add(Bq.Nat.add(field_183, b_1), c_2), Bq.Nat.add(field_183, Bq.Nat.add(b_1, c_2)), Bq.Nat.add_assoc(field_183, b_1, c_2)) : {Succ{_} == Succ{Bq.Nat.add(field_183, Bq.Nat.add(b_1, c_2))} : Nat}; {==})
729	
730	law Bq.Bag.add_assoc:
731	  (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> (@+c_2: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(a_0, b_1), c_2) == Bq.Bag.add(a_0, Bq.Bag.add(b_1, c_2)) : Bq.Bag})))
732	
733	def Bq.Bag.add_assoc(a_0, b_1, c_2):
734	  match a_0:
735	    case Con{field_184, field_185}:
736	      match b_1:
737	        case Con{field_186, field_187}:
738	          match c_2:
739	            case Con{field_188, field_189}:
740	              (%Equal.sym(Nat, Bq.Nat.add(Bq.Nat.add(field_184, field_186), field_188), Bq.Nat.add(field_184, Bq.Nat.add(field_186, field_188)), Bq.Nat.add_assoc(field_184, field_186, field_188)) : {Con{_, Bq.Bag.add(Bq.Bag.add(field_185, field_187), field_189)} == Con{Bq.Nat.add(field_184, Bq.Nat.add(field_186, field_188)), Bq.Bag.add(field_185, Bq.Bag.add(field_187, field_189))} : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(Bq.Bag.add(field_185, field_187), field_189), Bq.Bag.add(field_185, Bq.Bag.add(field_187, field_189)), Bq.Bag.add_assoc(field_185, field_187, field_189)) : {Con{Bq.Nat.add(field_184, Bq.Nat.add(field_186, field_188)), _} == Con{Bq.Nat.add(field_184, Bq.Nat.add(field_186, field_188)), Bq.Bag.add(field_185, Bq.Bag.add(field_187, field_189))} : List<&2, Nat>}; {==}))
741	            case Nil{}:
742	              {==}
743	        case Nil{}:
744	          {==}
745	    case Nil{}:
746	      {==}
747	
748	law Bq.bag_swap:
749	  (@+x_0: Bq.Bag -> (@+y_1: Bq.Bag -> (@+z_2: Bq.Bag -> {Bq.Bag.add(x_0, Bq.Bag.add(y_1, z_2)) == Bq.Bag.add(y_1, Bq.Bag.add(x_0, z_2)) : Bq.Bag})))
750	
751	def Bq.bag_swap(x_0, y_1, z_2):
752	  (%Equal.sym(Bq.Bag, Bq.Bag.add(x_0, Bq.Bag.add(y_1, z_2)), Bq.Bag.add(Bq.Bag.add(y_1, z_2), x_0), Bq.Bag.add_comm(x_0, Bq.Bag.add(y_1, z_2))) : {_ == Bq.Bag.add(y_1, Bq.Bag.add(x_0, z_2)) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(Bq.Bag.add(y_1, z_2), x_0), Bq.Bag.add(y_1, Bq.Bag.add(z_2, x_0)), Bq.Bag.add_assoc(y_1, z_2, x_0)) : {_ == Bq.Bag.add(y_1, Bq.Bag.add(x_0, z_2)) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(z_2, x_0), Bq.Bag.add(x_0, z_2), Bq.Bag.add_comm(z_2, x_0)) : {Bq.Bag.add(y_1, _) == Bq.Bag.add(y_1, Bq.Bag.add(x_0, z_2)) : List<&2, Nat>}; {==})))
753	
754	law Bq.Bool.BoolD:
755	  (@+x_0: Bool -> (@tc_1: Data -> (@fc_2: Data -> Data)))
756	
757	def Bq.Bool.BoolD(x_0, tc_1, fc_2):
758	  match x_0:
759	    case True{}:
760	      tc_1
761	    case False{}:
762	      fc_2
763	
764	law Bq.Bool.false_ne_true:
765	  (@+e_0: {False{} == True{} : Bool} -> Empty)
766	
767	def Bq.Bool.false_ne_true(e_0):
768	  (%Equal.sym(Bool, False{}, True{}, e_0) : Bq.Bool.BoolD(_, Unit, Empty); Unit{})
769	
770	law Bq.Nat.add_sub_cancel:
771	  (@+x_0: Nat -> (@+y_1: Nat -> (@+__2: {Bq.Nat.le(x_0, y_1) == True{} : Bool} -> {Bq.Nat.add(x_0, Bq.Nat.sub(y_1, x_0)) == y_1 : Nat})))
772	
773	def Bq.Nat.add_sub_cancel(x_0, y_1, __2):
774	  match x_0:
775	    case Zero{}:
776	      match y_1:
777	        case Zero{}:
778	          {==}
779	        case Succ{field_190}:
780	          {==}
781	    case Succ{field_191}:
782	      match y_1:
783	        case Zero{}:
784	          (apply_24 = {(xp_0 => \{}) : (@-xp_0: Nat -> (@+___1: Empty -> {Succ{Bq.Nat.add(xp_0, 0n)} == 0n : Nat}))}; apply_24(field_191, Bq.Bool.false_ne_true(__2)))
785	        case Succ{field_192}:
786	          (%Equal.sym(Nat, Bq.Nat.add(field_191, Bq.Nat.sub(field_192, field_191)), field_192, Bq.Nat.add_sub_cancel(field_191, field_192, __2)) : {Succ{_} == Succ{field_192} : Nat}; {==})
787	
788	law Bq.Bool.and_l:
789	  (@+x_0: Bool -> (@+y_1: Bool -> (@+e_2: {Bq.Bool.and(x_0, y_1) == True{} : Bool} -> {x_0 == True{} : Bool})))
790	
791	def Bq.Bool.and_l(x_0, y_1, e_2):
792	  match x_0:
793	    case True{}:
794	      {==}
795	    case False{}:
796	      e_2
797	
798	law Bq.Bool.and_r:
799	  (@+x_0: Bool -> (@+y_1: Bool -> (@+e_2: {Bq.Bool.and(x_0, y_1) == True{} : Bool} -> {y_1 == True{} : Bool})))
800	
801	def Bq.Bool.and_r(x_0, y_1, e_2):
802	  match x_0:
803	    case True{}:
804	      e_2
805	    case False{}:
806	      match y_1:
807	        case True{}:
808	          {==}
809	        case False{}:
810	          e_2
811	
812	law Bq.Bag.add_sub_cancel:
813	  (@+a_0: Bq.Bag -> (@+b_1: Bq.Bag -> (@+__2: {Bq.Bag.le(a_0, b_1) == True{} : Bool} -> {Bq.Bag.add(a_0, Bq.Bag.sub(b_1, a_0)) == b_1 : Bq.Bag})))
814	
815	def Bq.Bag.add_sub_cancel(a_0, b_1, __2):
816	  match a_0:
817	    case Con{field_193, field_194}:
818	      match b_1:
819	        case Con{field_195, field_196}:
820	          (%Equal.sym(Nat, Bq.Nat.add(field_193, Bq.Nat.sub(field_195, field_193)), field_195, Bq.Nat.add_sub_cancel(field_193, field_195, Bq.Bool.and_l(Bq.Nat.le(field_193, field_195), Bq.Bag.le(field_194, field_196), __2))) : {Con{_, Bq.Bag.add(field_194, Bq.Bag.sub(field_196, field_194))} == Con{field_195, field_196} : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(field_194, Bq.Bag.sub(field_196, field_194)), field_196, Bq.Bag.add_sub_cancel(field_194, field_196, Bq.Bool.and_r(Bq.Nat.le(field_193, field_195), Bq.Bag.le(field_194, field_196), __2))) : {Con{field_195, _} == Con{field_195, field_196} : List<&2, Nat>}; {==}))
821	        case Nil{}:
822	          (apply_25 = {(x_0 => (xs_1 => \{})) : (@-x_0: Nat -> (@-xs_1: List<&2, Nat> -> (@+___2: Empty -> {Con{x_0, xs_1} == Nil{} : List<&2, Nat>})))}; apply_25(field_193, field_194, Bq.Bool.false_ne_true(__2)))
823	    case Nil{}:
824	      match b_1:
825	        case Con{field_197, field_198}:
826	          {==}
827	        case Nil{}:
828	          {==}
829	
830	law Bq.equip_shuffle:
831	  (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+r_2: Bq.Bag -> (@+has_3: {Bq.Bag.le(k1_1, i_0) == True{} : Bool} -> {Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), Bq.Bag.add(k1_1, r_2)) == Bq.Bag.add(i_0, r_2) : Bq.Bag}))))
832	
833	def Bq.equip_shuffle(i_0, k1_1, r_2, has_3):
834	  (%Equal.sym(Bq.Bag, Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), Bq.Bag.add(k1_1, r_2)), Bq.Bag.add(k1_1, Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), r_2)), Bq.bag_swap(Bq.Bag.sub(i_0, k1_1), k1_1, r_2)) : {_ == Bq.Bag.add(i_0, r_2) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(k1_1, Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), r_2)), Bq.Bag.add(Bq.Bag.add(k1_1, Bq.Bag.sub(i_0, k1_1)), r_2), Equal.sym(Bq.Bag, Bq.Bag.add(Bq.Bag.add(k1_1, Bq.Bag.sub(i_0, k1_1)), r_2), Bq.Bag.add(k1_1, Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), r_2)), Bq.Bag.add_assoc(k1_1, Bq.Bag.sub(i_0, k1_1), r_2))) : {_ == Bq.Bag.add(i_0, r_2) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(k1_1, Bq.Bag.sub(i_0, k1_1)), i_0, Bq.Bag.add_sub_cancel(k1_1, i_0, has_3)) : {Bq.Bag.add(_, r_2) == Bq.Bag.add(i_0, r_2) : List<&2, Nat>}; {==})))
835	
836	law Bq.equip_shuffle_chm:
837	  (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+w_2: Bq.Bag -> (@+a_3: Bq.Bag -> (@+hb_4: Bq.Bag -> (@+has_5: {Bq.Bag.le(k1_1, i_0) == True{} : Bool} -> {Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, k1_1)))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, Nil{})))) : Bq.Bag}))))))
838	
839	def Bq.equip_shuffle_chm(i_0, k1_1, w_2, a_3, hb_4, has_5):
840	  (%Equal.sym(Bq.Bag, Bq.Bag.add(hb_4, Nil{}), hb_4, Bq.Bag.add_nil(hb_4)) : {Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, k1_1)))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, _))) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(hb_4, k1_1), Bq.Bag.add(k1_1, hb_4), Bq.Bag.add_comm(hb_4, k1_1)) : {Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), Bq.Bag.add(w_2, Bq.Bag.add(a_3, _))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4))) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(a_3, Bq.Bag.add(k1_1, hb_4)), Bq.Bag.add(k1_1, Bq.Bag.add(a_3, hb_4)), Bq.bag_swap(a_3, k1_1, hb_4)) : {Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), Bq.Bag.add(w_2, _)) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4))) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(w_2, Bq.Bag.add(k1_1, Bq.Bag.add(a_3, hb_4))), Bq.Bag.add(k1_1, Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4))), Bq.bag_swap(w_2, k1_1, Bq.Bag.add(a_3, hb_4))) : {Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), _) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4))) : List<&2, Nat>}; Bq.equip_shuffle(i_0, k1_1, Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4)), has_5)))))
841	
842	law Bq.equip_preserves_census:
843	  (@+k_0: Nat -> (@+h_1: Bq.Hero -> {Bq.census(Bq.hero_step(Bq.HOp.Equip{k_0}, h_1)) == Bq.census(h_1) : Bq.Bag}))
844	
845	def Bq.equip_preserves_census(k_0, h_1):
846	  match h_1:
847	    case Bq.Hero.Hero{field_199, field_200, field_201, field_202, field_203, field_204, field_205, field_206, field_207, field_208, field_209}:
848	      (apply_26 = {(k_0 => (inv_1 => (wea_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => \{Bq.ISlot.SlotNone: (ei_12 => {==}); \{Bq.ISlot.SlotW: (ei_12 => (apply_27 = {(k_0 => (inv_1 => (wea_2 => (lv_3 => (str_4 => (agi_5 => (vit_6 => (arm_7 => (hel_8 => (chm_9 => (gold_10 => (pts_11 => (ei_12 => \{False: (has_13 => {==}); \{True: (apply_28 = {(k_0 => (inv_1 => (lv_2 => (str_3 => (agi_4 => (vit_5 => (arm_6 => (hel_7 => (chm_8 => (gold_9 => (pts_10 => (ei_11 => \{Done: (value_12 => (has_13 => {==})); \{Fail: (error_12 => (has_13 => (apply_29 = {(k_0 => (inv_1 => (error_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => (ei_12 => (has_13 => \{False: {==}; \{True: (%Equal.sym(Bq.ISlot, (apply_30 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => slot_0)))))))); \{}} : (@+___0: Bq.Info -> Bq.ISlot)}; apply_30(Bq.item_info(k_0))), Bq.ISlot.SlotW{}, ei_12) : {Bq.census((apply_31 = {(inv_0 => (k_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => (wea_11 => \{Bq.ISlot.SlotW: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), Bq.Maybe.some(Nat, k_1), arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotA: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), wea_11, Bq.Maybe.some(Nat, k_1), hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotH: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), wea_11, arm_2, Bq.Maybe.some(Nat, k_1), chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotC: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), wea_11, arm_2, hel_3, Bq.Maybe.some(Nat, k_1), gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotNone: Bq.Hero.Hero{inv_0, wea_11, arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{}}}}}})))))))))))) : (@+inv_0: Bq.Bag -> (@+k_1: Nat -> (@+arm_2: Bq.Maybe(Nat) -> (@+hel_3: Bq.Maybe(Na
849	
850	law Bq.unequip_shuffle:
851	  (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+r_2: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), r_2) == Bq.Bag.add(i_0, Bq.Bag.add(k1_1, r_2)) : Bq.Bag})))
852	
853	def Bq.unequip_shuffle(i_0, k1_1, r_2):
854	  (%Equal.sym(Bq.Bag, Bq.Bag.add(Bq.Bag.add(k1_1, i_0), r_2), Bq.Bag.add(k1_1, Bq.Bag.add(i_0, r_2)), Bq.Bag.add_assoc(k1_1, i_0, r_2)) : {_ == Bq.Bag.add(i_0, Bq.Bag.add(k1_1, r_2)) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(k1_1, Bq.Bag.add(i_0, r_2)), Bq.Bag.add(i_0, Bq.Bag.add(k1_1, r_2)), Bq.bag_swap(k1_1, i_0, r_2)) : {_ == Bq.Bag.add(i_0, Bq.Bag.add(k1_1, r_2)) : List<&2, Nat>}; {==}))
855	
856	law Bq.unequip_shuffle2:
857	  (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+w_2: Bq.Bag -> (@+g_3: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, g_3)) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(k1_1, g_3))) : Bq.Bag}))))
858	
859	def Bq.unequip_shuffle2(i_0, k1_1, w_2, g_3):
860	  (%Equal.sym(Bq.Bag, Bq.Bag.add(w_2, Bq.Bag.add(k1_1, g_3)), Bq.Bag.add(k1_1, Bq.Bag.add(w_2, g_3)), Bq.bag_swap(w_2, k1_1, g_3)) : {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, g_3)) == Bq.Bag.add(i_0, _) : List<&2, Nat>}; Bq.unequip_shuffle(i_0, k1_1, Bq.Bag.add(w_2, g_3)))
861	
862	law Bq.unequip_shuffle3:
863	  (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+w_2: Bq.Bag -> (@+a_3: Bq.Bag -> (@+g_4: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, g_4))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(k1_1, g_4)))) : Bq.Bag})))))
864	
865	def Bq.unequip_shuffle3(i_0, k1_1, w_2, a_3, g_4):
866	  (%Equal.sym(Bq.Bag, Bq.Bag.add(a_3, Bq.Bag.add(k1_1, g_4)), Bq.Bag.add(k1_1, Bq.Bag.add(a_3, g_4)), Bq.bag_swap(a_3, k1_1, g_4)) : {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, g_4))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, _)) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(w_2, Bq.Bag.add(k1_1, Bq.Bag.add(a_3, g_4))), Bq.Bag.add(k1_1, Bq.Bag.add(w_2, Bq.Bag.add(a_3, g_4))), Bq.bag_swap(w_2, k1_1, Bq.Bag.add(a_3, g_4))) : {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, g_4))) == Bq.Bag.add(i_0, _) : List<&2, Nat>}; Bq.unequip_shuffle(i_0, k1_1, Bq.Bag.add(w_2, Bq.Bag.add(a_3, g_4)))))
867	
868	law Bq.unequip_shuffle4:
869	  (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+w_2: Bq.Bag -> (@+a_3: Bq.Bag -> (@+hb_4: Bq.Bag -> {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, Nil{})))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, k1_1)))) : Bq.Bag})))))
870	
871	def Bq.unequip_shuffle4(i_0, k1_1, w_2, a_3, hb_4):
872	  (%Equal.sym(Bq.Bag, Bq.Bag.add(hb_4, Nil{}), hb_4, Bq.Bag.add_nil(hb_4)) : {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, _))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, Bq.Bag.add(hb_4, k1_1)))) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(hb_4, k1_1), Bq.Bag.add(k1_1, hb_4), Bq.Bag.add_comm(hb_4, k1_1)) : {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, Bq.Bag.add(a_3, _))) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(a_3, Bq.Bag.add(k1_1, hb_4)), Bq.Bag.add(k1_1, Bq.Bag.add(a_3, hb_4)), Bq.bag_swap(a_3, k1_1, hb_4)) : {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4))) == Bq.Bag.add(i_0, Bq.Bag.add(w_2, _)) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(w_2, Bq.Bag.add(k1_1, Bq.Bag.add(a_3, hb_4))), Bq.Bag.add(k1_1, Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4))), Bq.bag_swap(w_2, k1_1, Bq.Bag.add(a_3, hb_4))) : {Bq.Bag.add(Bq.Bag.add(k1_1, i_0), Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4))) == Bq.Bag.add(i_0, _) : List<&2, Nat>}; Bq.unequip_shuffle(i_0, k1_1, Bq.Bag.add(w_2, Bq.Bag.add(a_3, hb_4)))))))
873	
874	law Bq.unequip_preserves_census:
875	  (@+s_0: Bq.ISlot -> (@+h_1: Bq.Hero -> {Bq.census(Bq.hero_step(Bq.HOp.Unequip{s_0}, h_1)) == Bq.census(h_1) : Bq.Bag}))
876	
877	def Bq.unequip_preserves_census(s_0, h_1):
878	  match h_1:
879	    case Bq.Hero.Hero{field_210, field_211, field_212, field_213, field_214, field_215, field_216, field_217, field_218, field_219, field_220}:
880	      (apply_97 = {\{Bq.ISlot.SlotNone: (inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => {==}))))))))))); \{Bq.ISlot.SlotW: (inv_0 => \{Fail: (u_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => {==})))))))))); \{Done: (k0_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => Bq.unequip_shuffle(inv_0, Bq.one(k0_1), Bq.Bag.add(Bq.mb(arm_2), Bq.Bag.add(Bq.mb(hel_3), Bq.mb(chm_4)))))))))))))); \{}}}); \{Bq.ISlot.SlotA: (inv_0 => (wea_1 => \{Fail: (u_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => {==}))))))))); \{Done: (k0_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => Bq.unequip_shuffle2(inv_0, Bq.one(k0_2), Bq.mb(wea_1), Bq.Bag.add(Bq.mb(hel_3), Bq.mb(chm_4)))))))))))); \{}}})); \{Bq.ISlot.SlotH: (inv_0 => (wea_1 => (arm_2 => \{Fail: (u_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => {==})))))))); \{Done: (k0_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => Bq.unequip_shuffle3(inv_0, Bq.one(k0_3), Bq.mb(wea_1), Bq.mb(arm_2), Bq.mb(chm_4)))))))))); \{}}}))); \{Bq.ISlot.SlotC: (inv_0 => (wea_1 => (arm_2 => (hel_3 => \{Fail: (u_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => {==}))))))); \{Done: (k0_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => Bq.unequip_shuffle4(inv_0, Bq.one(k0_4), Bq.mb(wea_1), Bq.mb(arm_2), Bq.mb(hel_3))))))))); \{}}})))); \{}}}}}} : (@+___0: Bq.ISlot -> (@+__1: List<&2, Nat> -> (@+__2: Result<&2, &2, Unit, Nat> -> (@+__3: Result<&2, &2, Unit, Nat> -> (@+__4: Result<&2, &2, Unit, Nat> -> (@+__5: Result<&2, &2, Unit, Nat> -> (@+__6: Nat -> (@+__7: Nat -> (@+__8: Nat -> (@+__9: Nat -> (@+__10: Nat -> (@+__11: Nat -> {Bq.census(Bq.hero_step_go(Bq.Bool.not(Bq.slot_empty(Bq.slot_of(Bq.Hero.Hero{__1, __2, __3, __4, __5, __6, __7, __8, __9, 
881	
882	law Bq.transfer:
883	  (@+op_0: Bq.HOp -> Bool)
884	
885	def Bq.transfer(op_0):
886	  match op_0:
887	    case Bq.HOp.Equip{field_221}:
888	      True{}
889	    case Bq.HOp.Unequip{field_222}:
890	      True{}
891	    case Bq.HOp.Buy{field_223}:
892	      False{}
893	    case Bq.HOp.Quaff{}:
894	      False{}
895	    case Bq.HOp.Alloc{field_224}:
896	      False{}
897	    case Bq.HOp.LevelUp{}:
898	      False{}
899	
900	law Bq.transfers:
901	  (@+ops_0: List<&2, Bq.HOp> -> Bool)
902	
903	def Bq.transfers(ops_0):
904	  match ops_0:
905	    case Nil{}:
906	      True{}
907	    case Con{field_225, field_226}:
908	      Bq.Bool.and(Bq.transfer(field_225), Bq.transfers(field_226))
909	
910	law Bq.hero_run:
911	  (@+ops_0: List<&2, Bq.HOp> -> (@+h_1: Bq.Hero -> Bq.Hero))
912	
913	def Bq.hero_run(ops_0, h_1):
914	  match ops_0:
915	    case Nil{}:
916	      h_1
917	    case Con{field_227, field_228}:
918	      Bq.hero_run(field_228, Bq.hero_step(field_227, h_1))
919	
920	law Bq.transfers_preserve_census:
921	  (@+ops_0: List<&2, Bq.HOp> -> (@+__1: {Bq.transfers(ops_0) == True{} : Bool} -> (@+h_2: Bq.Hero -> {Bq.census(Bq.hero_run(ops_0, h_2)) == Bq.census(h_2) : Bq.Bag})))
922	
923	def Bq.transfers_preserve_census(ops_0, __1, h_2):
924	  match ops_0:
925	    case Nil{}:
926	      {==}
927	    case Con{field_229, field_230}:
928	      match field_229:
929	        case Bq.HOp.Equip{field_231}:
930	          (%Equal.sym(Bq.Bag, Bq.census(Bq.hero_run(field_230, Bq.hero_step(Bq.HOp.Equip{field_231}, h_2))), Bq.census(Bq.hero_step(Bq.HOp.Equip{field_231}, h_2)), Bq.transfers_preserve_census(field_230, __1, Bq.hero_step(Bq.HOp.Equip{field_231}, h_2))) : {_ == Bq.census(h_2) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.census(Bq.hero_step(Bq.HOp.Equip{field_231}, h_2)), Bq.census(h_2), Bq.equip_preserves_census(field_231, h_2)) : {_ == Bq.census(h_2) : List<&2, Nat>}; {==}))
931	        case Bq.HOp.Unequip{field_232}:
932	          (%Equal.sym(Bq.Bag, Bq.census(Bq.hero_run(field_230, Bq.hero_step(Bq.HOp.Unequip{field_232}, h_2))), Bq.census(Bq.hero_step(Bq.HOp.Unequip{field_232}, h_2)), Bq.transfers_preserve_census(field_230, __1, Bq.hero_step(Bq.HOp.Unequip{field_232}, h_2))) : {_ == Bq.census(h_2) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.census(Bq.hero_step(Bq.HOp.Unequip{field_232}, h_2)), Bq.census(h_2), Bq.unequip_preserves_census(field_232, h_2)) : {_ == Bq.census(h_2) : List<&2, Nat>}; {==}))
933	        case Bq.HOp.Buy{field_233}:
934	          (apply_98 = {(rest_0 => (k_1 => (h_2 => \{}))) : (@-rest_0: List<&2, Bq.HOp> -> (@-k_1: Nat -> (@-h_2: Bq.Hero -> (@+___3: Empty -> {Bq.census(Bq.hero_run(rest_0, Bq.hero_step_go(Bq.Bool.and(Bq.Nat.le(1n, (apply_99 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => price_7)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_99(Bq.item_info(k_1)))), Bq.Nat.le((apply_100 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => price_7)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_100(Bq.item_info(k_1))), Bq.hero_gold(h_2))), Bq.HOp.Buy{k_1}, h_2))) == Bq.census(h_2) : List<&2, Nat>}))))}; apply_98(field_230, field_233, h_2, Bq.Bool.false_ne_true(__1)))
935	        case Bq.HOp.Quaff{}:
936	          (apply_101 = {(rest_0 => (h_1 => \{})) : (@-rest_0: List<&2, Bq.HOp> -> (@-h_1: Bq.Hero -> (@+___2: Empty -> {Bq.census(Bq.hero_run(rest_0, Bq.hero_step_go(Bq.quaff_ok(h_1), Bq.HOp.Quaff{}, h_1))) == Bq.census(h_1) : List<&2, Nat>})))}; apply_101(field_230, h_2, Bq.Bool.false_ne_true(__1)))
937	        case Bq.HOp.Alloc{field_234}:
938	          (apply_102 = {(rest_0 => (h_1 => (s_2 => \{}))) : (@-rest_0: List<&2, Bq.HOp> -> (@-h_1: Bq.Hero -> (@-s_2: Nat -> (@+___3: Empty -> {Bq.census(Bq.hero_run(rest_0, Bq.hero_step_go(Bq.alloc_ok(h_1), Bq.HOp.Alloc{s_2}, h_1))) == Bq.census(h_1) : List<&2, Nat>}))))}; apply_102(field_230, h_2, field_234, Bq.Bool.false_ne_true(__1)))
939	        case Bq.HOp.LevelUp{}:
940	          (apply_103 = {(rest_0 => (h_1 => \{})) : (@-rest_0: List<&2, Bq.HOp> -> (@-h_1: Bq.Hero -> (@+___2: Empty -> {Bq.census(Bq.hero_run(rest_0, Bq.do_levelup(h_1))) == Bq.census(h_1) : List<&2, Nat>})))}; apply_103(field_230, h_2, Bq.Bool.false_ne_true(__1)))
941	
942	law Bq.buy_mints_exactly_one:
943	  (@+k_0: Nat -> (@+h_1: Bq.Hero -> (@+__2: {Bq.buy_ok(k_0, h_1) == True{} : Bool} -> {Bq.census(Bq.hero_step(Bq.HOp.Buy{k_0}, h_1)) == Bq.Bag.add(Bq.one(k_0), Bq.census(h_1)) : Bq.Bag})))
944	
945	def Bq.buy_mints_exactly_one(k_0, h_1, __2):
946	  match h_1:
947	    case Bq.Hero.Hero{field_235, field_236, field_237, field_238, field_239, field_240, field_241, field_242, field_243, field_244, field_245}:
948	      (%Equal.sym(Bool, Bq.buy_ok(k_0, Bq.Hero.Hero{field_235, field_236, field_237, field_238, field_239, field_240, field_241, field_242, field_243, field_244, field_245}), True{}, __2) : {Bq.census(Bq.hero_step_go(_, Bq.HOp.Buy{k_0}, Bq.Hero.Hero{field_235, field_236, field_237, field_238, field_239, field_240, field_241, field_242, field_243, field_244, field_245})) == Bq.Bag.add(Bq.one(k_0), Bq.Bag.add(field_235, Bq.Bag.add(Bq.mb(field_236), Bq.Bag.add(Bq.mb(field_237), Bq.Bag.add(Bq.mb(field_238), Bq.mb(field_239)))))) : List<&2, Nat>}; Bq.Bag.add_assoc(Bq.one(k_0), field_235, Bq.gear_bag(field_236, field_237, field_238, field_239)))
949	
950	law Bq.buy_burns_exact_gold:
951	  (@+k_0: Nat -> (@+h_1: Bq.Hero -> (@+__2: {Bq.buy_ok(k_0, h_1) == True{} : Bool} -> {Bq.Nat.add(Bq.iprice(k_0), Bq.hero_gold(Bq.hero_step(Bq.HOp.Buy{k_0}, h_1))) == Bq.hero_gold(h_1) : Nat})))
952	
953	def Bq.buy_burns_exact_gold(k_0, h_1, __2):
954	  match h_1:
955	    case Bq.Hero.Hero{field_246, field_247, field_248, field_249, field_250, field_251, field_252, field_253, field_254, field_255, field_256}:
956	      (+ev_13 = Bq.Bool.and_r(Bq.Nat.lt(0n, Bq.iprice(k_0)), Bq.Nat.le(Bq.iprice(k_0), field_251), __2); (%Equal.sym(Bool, Bq.buy_ok(k_0, Bq.Hero.Hero{field_246, field_247, field_248, field_249, field_250, field_251, field_252, field_253, field_254, field_255, field_256}), True{}, __2) : {Bq.Nat.add((apply_104 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => price_7)))))))); \{}} : (@+___0: Bq.Info -> Nat)}; apply_104(Bq.item_info(k_0))), Bq.hero_gold(Bq.hero_step_go(_, Bq.HOp.Buy{k_0}, Bq.Hero.Hero{field_246, field_247, field_248, field_249, field_250, field_251, field_252, field_253, field_254, field_255, field_256}))) == field_251 : Nat}; Bq.Nat.add_sub_cancel(Bq.iprice(k_0), field_251, ev_13)))
957	
958	law Bq.and_intro:
959	  (@+x_0: Bool -> (@+y_1: Bool -> (@+ex_2: {x_0 == True{} : Bool} -> (@+ey_3: {y_1 == True{} : Bool} -> {Bq.Bool.and(x_0, y_1) == True{} : Bool}))))
960	
961	def Bq.and_intro(x_0, y_1, ex_2, ey_3):
962	  (%Equal.sym(Bool, x_0, True{}, ex_2) : {Bq.Bool.and(_, y_1) == True{} : Bool}; (%Equal.sym(Bool, y_1, True{}, ey_3) : {_ == True{} : Bool}; {==}))
963	
964	law Bq.shop_never_refuses_a_funded_buy:
965	  (@+k_0: Nat -> (@+__1: {Bq.Nat.lt(0n, Bq.iprice(k_0)) == True{} : Bool} -> (@+h_2: Bq.Hero -> (@+__3: {Bq.Nat.le(Bq.iprice(k_0), Bq.hero_gold(h_2)) == True{} : Bool} -> {Bq.census(Bq.hero_step(Bq.HOp.Buy{k_0}, h_2)) == Bq.Bag.add(Bq.one(k_0), Bq.census(h_2)) : Bq.Bag}))))
966	
967	def Bq.shop_never_refuses_a_funded_buy(k_0, __1, h_2, __3):
968	  Bq.buy_mints_exactly_one(k_0, h_2, Bq.and_intro(Bq.Nat.lt(0n, Bq.iprice(k_0)), Bq.Nat.le(Bq.iprice(k_0), Bq.hero_gold(h_2)), __1, __3))
969	
970	law Bq.quaff_burns_one_potion:
971	  (@+h_0: Bq.Hero -> (@+__1: {Bq.quaff_ok(h_0) == True{} : Bool} -> {Bq.Bag.add(Bq.one(Bq.POTION), Bq.census(Bq.hero_step(Bq.HOp.Quaff{}, h_0))) == Bq.census(h_0) : Bq.Bag}))
972	
973	def Bq.quaff_burns_one_potion(h_0, __1):
974	  match h_0:
975	    case Bq.Hero.Hero{field_257, field_258, field_259, field_260, field_261, field_262, field_263, field_264, field_265, field_266, field_267}:
976	      (apply_105 = {(inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => (e_11 => \{True: (has_12 => (%Equal.sym(Bq.Bag, Bq.Bag.add(Bq.one(0n), Bq.Bag.add(Bq.Bag.sub(inv_0, Bq.one(0n)), Bq.gear_bag(wea_1, arm_2, hel_3, chm_4))), Bq.Bag.add(Bq.Bag.add(Bq.one(0n), Bq.Bag.sub(inv_0, Bq.one(0n))), Bq.gear_bag(wea_1, arm_2, hel_3, chm_4)), Equal.sym(Bq.Bag, Bq.Bag.add(Bq.Bag.add(Bq.one(0n), Bq.Bag.sub(inv_0, Bq.one(0n))), Bq.gear_bag(wea_1, arm_2, hel_3, chm_4)), Bq.Bag.add(Bq.one(0n), Bq.Bag.add(Bq.Bag.sub(inv_0, Bq.one(0n)), Bq.gear_bag(wea_1, arm_2, hel_3, chm_4))), Bq.Bag.add_assoc(Bq.one(0n), Bq.Bag.sub(inv_0, Bq.one(0n)), Bq.gear_bag(wea_1, arm_2, hel_3, chm_4)))) : {_ == Bq.Bag.add(inv_0, Bq.Bag.add(Bq.mb(wea_1), Bq.Bag.add(Bq.mb(arm_2), Bq.Bag.add(Bq.mb(hel_3), Bq.mb(chm_4))))) : List<&2, Nat>}; (%Equal.sym(Bq.Bag, Bq.Bag.add(Bq.one(0n), Bq.Bag.sub(inv_0, Bq.one(0n))), inv_0, Bq.Bag.add_sub_cancel(Bq.one(0n), inv_0, has_12)) : {Bq.Bag.add(_, Bq.Bag.add(Bq.mb(wea_1), Bq.Bag.add(Bq.mb(arm_2), Bq.Bag.add(Bq.mb(hel_3), Bq.mb(chm_4))))) == Bq.Bag.add(inv_0, Bq.Bag.add(Bq.mb(wea_1), Bq.Bag.add(Bq.mb(arm_2), Bq.Bag.add(Bq.mb(hel_3), Bq.mb(chm_4))))) : List<&2, Nat>}; {==}))); \{False: (has_12 => (apply_106 = {(inv_0 => (wea_1 => (arm_2 => (hel_3 => (chm_4 => \{}))))) : (@-inv_0: Bq.Bag -> (@-wea_1: Bq.Maybe(Nat) -> (@-arm_2: Bq.Maybe(Nat) -> (@-hel_3: Bq.Maybe(Nat) -> (@-chm_4: Bq.Maybe(Nat) -> (@+___5: Empty -> {Bq.Bag.add([1n], Bq.Bag.add(inv_0, Bq.Bag.add(Bq.mb(wea_1), Bq.Bag.add(Bq.mb(arm_2), Bq.Bag.add(Bq.mb(hel_3), Bq.mb(chm_4)))))) == Bq.Bag.add(inv_0, Bq.Bag.add(Bq.mb(wea_1), Bq.Bag.add(Bq.mb(arm_2), Bq.Bag.add(Bq.mb(hel_3), Bq.mb(chm_4))))) : List<&2, Nat>}))))))}; apply_106(inv_0, wea_1, arm_2, hel_3, chm_4, Bq.Bool.false_ne_true(Equal.trans(Bool, False{}, Bq.Bag.le([1n], inv_0), True{}, Equal.sym(Bool, Bq.Bag.le([1n], inv_0), False{}, has_12), e_11))))); \{}}})))))))))))) : (@+inv_0: Bq.Bag -> (@+wea_1
977	
978	law Bq.stat_total:
979	  (@+h_0: Bq.Hero -> Nat)
980	
981	def Bq.stat_total(h_0):
982	  match h_0:
983	    case Bq.Hero.Hero{field_268, field_269, field_270, field_271, field_272, field_273, field_274, field_275, field_276, field_277, field_278}:
984	      Bq.Nat.add(field_275, Bq.Nat.add(field_276, Bq.Nat.add(field_277, field_278)))
985	
986	law Bq.stat_expect:
987	  (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> Nat))
988	
989	def Bq.stat_expect(op_0, h_1):
990	  match op_0:
991	    case Bq.HOp.LevelUp{}:
992	      Bq.Nat.add(3n, Bq.stat_total(h_1))
993	    case Bq.HOp.Equip{field_279}:
994	      Bq.stat_total(h_1)
995	    case Bq.HOp.Unequip{field_280}:
996	      Bq.stat_total(h_1)
997	    case Bq.HOp.Buy{field_281}:
998	      Bq.stat_total(h_1)
999	    case Bq.HOp.Quaff{}:
1000	      Bq.stat_total(h_1)
1001	    case Bq.HOp.Alloc{field_282}:
1002	      Bq.stat_total(h_1)
1003	
1004	law Bq.stat_succ:
1005	  (@+a_0: Nat -> (@+b_1: Nat -> (@+c_2: Nat -> (@+d_3: Nat -> {Bq.Nat.add(a_0, Bq.Nat.add(b_1, Bq.Nat.add(c_2, Succ{d_3}))) == Succ{Bq.Nat.add(a_0, Bq.Nat.add(b_1, Bq.Nat.add(c_2, d_3)))} : Nat}))))
1006	
1007	def Bq.stat_succ(a_0, b_1, c_2, d_3):
1008	  (%Equal.sym(Nat, Bq.Nat.add(c_2, Succ{d_3}), Succ{Bq.Nat.add(c_2, d_3)}, Bq.Nat.add_succ(c_2, d_3)) : {Bq.Nat.add(a_0, Bq.Nat.add(b_1, _)) == Succ{Bq.Nat.add(a_0, Bq.Nat.add(b_1, Bq.Nat.add(c_2, d_3)))} : Nat}; (%Equal.sym(Nat, Bq.Nat.add(b_1, Succ{Bq.Nat.add(c_2, d_3)}), Succ{Bq.Nat.add(b_1, Bq.Nat.add(c_2, d_3))}, Bq.Nat.add_succ(b_1, Bq.Nat.add(c_2, d_3))) : {Bq.Nat.add(a_0, _) == Succ{Bq.Nat.add(a_0, Bq.Nat.add(b_1, Bq.Nat.add(c_2, d_3)))} : Nat}; (%Equal.sym(Nat, Bq.Nat.add(a_0, Succ{Bq.Nat.add(b_1, Bq.Nat.add(c_2, d_3))}), Succ{Bq.Nat.add(a_0, Bq.Nat.add(b_1, Bq.Nat.add(c_2, d_3)))}, Bq.Nat.add_succ(a_0, Bq.Nat.add(b_1, Bq.Nat.add(c_2, d_3)))) : {_ == Succ{Bq.Nat.add(a_0, Bq.Nat.add(b_1, Bq.Nat.add(c_2, d_3)))} : Nat}; {==})))
1009	
1010	law Bq.ops_respect_stat_budget:
1011	  (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> {Bq.stat_total(Bq.hero_step(op_0, h_1)) == Bq.stat_expect(op_0, h_1) : Nat}))
1012	
1013	def Bq.ops_respect_stat_budget(op_0, h_1):
1014	  match h_1:
1015	    case Bq.Hero.Hero{field_283, field_284, field_285, field_286, field_287, field_288, field_289, field_290, field_291, field_292, field_293}:
1016	      (apply_107 = {\{Bq.HOp.Equip: (k_0 => (inv_1 => (wea_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => (apply_108 = {(k_0 => (inv_1 => (wea_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => \{Bq.ISlot.SlotNone: (ei_12 => {==}); \{Bq.ISlot.SlotW: (ei_12 => (apply_109 = {(wea_0 => (k_1 => (lv_2 => (str_3 => (agi_4 => (vit_5 => (inv_6 => (arm_7 => (hel_8 => (chm_9 => (gold_10 => (pts_11 => (ei_12 => \{False: {==}; \{True: (apply_110 = {(k_0 => (lv_1 => (str_2 => (agi_3 => (vit_4 => (inv_5 => (arm_6 => (hel_7 => (chm_8 => (gold_9 => (pts_10 => (ei_11 => \{Done: (value_12 => {==}); \{Fail: (error_12 => (apply_111 = {(k_0 => (inv_1 => (error_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => (ei_12 => \{False: {==}; \{True: (%Equal.sym(Bq.ISlot, (apply_112 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => slot_0)))))))); \{}} : (@+___0: Bq.Info -> Bq.ISlot)}; apply_112(Bq.item_info(k_0))), Bq.ISlot.SlotW{}, ei_12) : {Bq.stat_total((apply_113 = {(inv_0 => (k_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => (wea_11 => \{Bq.ISlot.SlotW: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), Bq.Maybe.some(Nat, k_1), arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotA: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), wea_11, Bq.Maybe.some(Nat, k_1), hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotH: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), wea_11, arm_2, Bq.Maybe.some(Nat, k_1), chm_4, gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotC: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), wea_11, arm_2, hel_3, Bq.Maybe.some(Nat, k_1), gold_5, lv_6, str_7, agi_8, vit_9, pts_10}; \{Bq.ISlot.SlotNone: Bq.Hero.Hero{inv_0, wea_11, arm_2, hel_3, chm_4, gold_5, lv_6, str_7, agi_8, vit_9, 
1017	
1018	law Bq.WearOK:
1019	  (@+m_0: Bq.Maybe(Nat) -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> Data)))))
1020	
1021	def Bq.WearOK(m_0, lv_1, str_2, agi_3, vit_4):
1022	  match m_0:
1023	    case Done{field_294}:
1024	      {Bq.can_wear(field_294, lv_1, str_2, agi_3, vit_4) == True{} : Bool}
1025	    case Fail{field_295}:
1026	      Unit
1027	
1028	law Bq.WellEquipped:
1029	  (@+h_0: Bq.Hero -> Data)
1030	
1031	def Bq.WellEquipped(h_0):
1032	  match h_0:
1033	    case Bq.Hero.Hero{field_296, field_297, field_298, field_299, field_300, field_301, field_302, field_303, field_304, field_305, field_306}:
1034	      Bq.Pair.Pair(Bq.WearOK(field_297, field_302, field_303, field_304, field_305), (__11 => Bq.Pair.Pair(Bq.WearOK(field_298, field_302, field_303, field_304, field_305), (__12 => Bq.Pair.Pair(Bq.WearOK(field_299, field_302, field_303, field_304, field_305), (__13 => Bq.WearOK(field_300, field_302, field_303, field_304, field_305)))))))
1035	
1036	law Bq.le_succ_r:
1037	  (@+a_0: Nat -> (@+b_1: Nat -> (@+e_2: {Bq.Nat.le(a_0, b_1) == True{} : Bool} -> {Bq.Nat.le(a_0, Succ{b_1}) == True{} : Bool})))
1038	
1039	def Bq.le_succ_r(a_0, b_1, e_2):
1040	  match a_0:
1041	    case Zero{}:
1042	      {==}
1043	    case Succ{field_307}:
1044	      match b_1:
1045	        case Zero{}:
1046	          (apply_190 = {(ap_0 => \{}) : (@-ap_0: Nat -> (@+___1: Empty -> {Bq.Nat.le(ap_0, 0n) == True{} : Bool}))}; apply_190(field_307, Bq.Bool.false_ne_true(e_2)))
1047	        case Succ{field_308}:
1048	          Bq.le_succ_r(field_307, field_308, e_2)
1049	
1050	law Bq.can_wear_mono_str:
1051	  (@+k_0: Nat -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> (@+e_5: {Bq.can_wear(k_0, lv_1, str_2, agi_3, vit_4) == True{} : Bool} -> {Bq.can_wear(k_0, lv_1, Succ{str_2}, agi_3, vit_4) == True{} : Bool}))))))
1052	
1053	def Bq.can_wear_mono_str(k_0, lv_1, str_2, agi_3, vit_4, e_5):
1054	  (+eL_6 = Bq.Bool.and_l(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), e_5); (+eR_7 = Bq.Bool.and_r(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), e_5); (+eS_8 = Bq.Bool.and_l(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4)), eR_7); (+e2_9 = Bq.Bool.and_r(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4)), eR_7); Bq.and_intro(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), Succ{str_2}), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), eL_6, Bq.and_intro(Bq.Nat.le(Bq.istreq(k_0), Succ{str_2}), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4)), Bq.le_succ_r(Bq.istreq(k_0), str_2, eS_8), e2_9))))))
1055	
1056	law Bq.wear_ok_mono_str:
1057	  (@+m_0: Bq.Maybe(Nat) -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> (@+wo_5: Bq.WearOK(m_0, lv_1, str_2, agi_3, vit_4) -> Bq.WearOK(m_0, lv_1, Succ{str_2}, agi_3, vit_4)))))))
1058	
1059	def Bq.wear_ok_mono_str(m_0, lv_1, str_2, agi_3, vit_4, wo_5):
1060	  match m_0:
1061	    case Done{field_309}:
1062	      Bq.can_wear_mono_str(field_309, lv_1, str_2, agi_3, vit_4, wo_5)
1063	    case Fail{field_310}:
1064	      Unit{}
1065	
1066	law Bq.can_wear_mono_agi:
1067	  (@+k_0: Nat -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> (@+e_5: {Bq.can_wear(k_0, lv_1, str_2, agi_3, vit_4) == True{} : Bool} -> {Bq.can_wear(k_0, lv_1, str_2, Succ{agi_3}, vit_4) == True{} : Bool}))))))
1068	
1069	def Bq.can_wear_mono_agi(k_0, lv_1, str_2, agi_3, vit_4, e_5):
1070	  (+eL_6 = Bq.Bool.and_l(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), e_5); (+eR_7 = Bq.Bool.and_r(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), e_5); (+eS_8 = Bq.Bool.and_l(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4)), eR_7); (+e2_9 = Bq.Bool.and_r(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4)), eR_7); (+eA_10 = Bq.Bool.and_l(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4), e2_9); (+eV_11 = Bq.Bool.and_r(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4), e2_9); Bq.and_intro(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), Succ{agi_3}), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), eL_6, Bq.and_intro(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), Succ{agi_3}), Bq.Nat.le(Bq.ivitreq(k_0), vit_4)), eS_8, Bq.and_intro(Bq.Nat.le(Bq.iagireq(k_0), Succ{agi_3}), Bq.Nat.le(Bq.ivitreq(k_0), vit_4), Bq.le_succ_r(Bq.iagireq(k_0), agi_3, eA_10), eV_11)))))))))
1071	
1072	law Bq.wear_ok_mono_agi:
1073	  (@+m_0: Bq.Maybe(Nat) -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> (@+wo_5: Bq.WearOK(m_0, lv_1, str_2, agi_3, vit_4) -> Bq.WearOK(m_0, lv_1, str_2, Succ{agi_3}, vit_4)))))))
1074	
1075	def Bq.wear_ok_mono_agi(m_0, lv_1, str_2, agi_3, vit_4, wo_5):
1076	  match m_0:
1077	    case Done{field_311}:
1078	      Bq.can_wear_mono_agi(field_311, lv_1, str_2, agi_3, vit_4, wo_5)
1079	    case Fail{field_312}:
1080	      Unit{}
1081	
1082	law Bq.can_wear_mono_vit:
1083	  (@+k_0: Nat -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> (@+e_5: {Bq.can_wear(k_0, lv_1, str_2, agi_3, vit_4) == True{} : Bool} -> {Bq.can_wear(k_0, lv_1, str_2, agi_3, Succ{vit_4}) == True{} : Bool}))))))
1084	
1085	def Bq.can_wear_mono_vit(k_0, lv_1, str_2, agi_3, vit_4, e_5):
1086	  (+eL_6 = Bq.Bool.and_l(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), e_5); (+eR_7 = Bq.Bool.and_r(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), e_5); (+eS_8 = Bq.Bool.and_l(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4)), eR_7); (+e2_9 = Bq.Bool.and_r(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4)), eR_7); (+eA_10 = Bq.Bool.and_l(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4), e2_9); (+eV_11 = Bq.Bool.and_r(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4), e2_9); Bq.and_intro(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), Succ{vit_4}))), eL_6, Bq.and_intro(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), Succ{vit_4})), eS_8, Bq.and_intro(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), Succ{vit_4}), eA_10, Bq.le_succ_r(Bq.ivitreq(k_0), vit_4, eV_11))))))))))
1087	
1088	law Bq.wear_ok_mono_vit:
1089	  (@+m_0: Bq.Maybe(Nat) -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> (@+wo_5: Bq.WearOK(m_0, lv_1, str_2, agi_3, vit_4) -> Bq.WearOK(m_0, lv_1, str_2, agi_3, Succ{vit_4})))))))
1090	
1091	def Bq.wear_ok_mono_vit(m_0, lv_1, str_2, agi_3, vit_4, wo_5):
1092	  match m_0:
1093	    case Done{field_313}:
1094	      Bq.can_wear_mono_vit(field_313, lv_1, str_2, agi_3, vit_4, wo_5)
1095	    case Fail{field_314}:
1096	      Unit{}
1097	
1098	law Bq.can_wear_mono_lv:
1099	  (@+k_0: Nat -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> (@+e_5: {Bq.can_wear(k_0, lv_1, str_2, agi_3, vit_4) == True{} : Bool} -> {Bq.can_wear(k_0, Succ{lv_1}, str_2, agi_3, vit_4) == True{} : Bool}))))))
1100	
1101	def Bq.can_wear_mono_lv(k_0, lv_1, str_2, agi_3, vit_4, e_5):
1102	  (+eL_6 = Bq.Bool.and_l(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), e_5); (+eR_7 = Bq.Bool.and_r(Bq.Nat.le(Bq.ilvreq(k_0), lv_1), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), e_5); Bq.and_intro(Bq.Nat.le(Bq.ilvreq(k_0), Succ{lv_1}), Bq.Bool.and(Bq.Nat.le(Bq.istreq(k_0), str_2), Bq.Bool.and(Bq.Nat.le(Bq.iagireq(k_0), agi_3), Bq.Nat.le(Bq.ivitreq(k_0), vit_4))), Bq.le_succ_r(Bq.ilvreq(k_0), lv_1, eL_6), eR_7)))
1103	
1104	law Bq.wear_ok_mono_lv:
1105	  (@+m_0: Bq.Maybe(Nat) -> (@+lv_1: Nat -> (@+str_2: Nat -> (@+agi_3: Nat -> (@+vit_4: Nat -> (@+wo_5: Bq.WearOK(m_0, lv_1, str_2, agi_3, vit_4) -> Bq.WearOK(m_0, Succ{lv_1}, str_2, agi_3, vit_4)))))))
1106	
1107	def Bq.wear_ok_mono_lv(m_0, lv_1, str_2, agi_3, vit_4, wo_5):
1108	  match m_0:
1109	    case Done{field_315}:
1110	      Bq.can_wear_mono_lv(field_315, lv_1, str_2, agi_3, vit_4, wo_5)
1111	    case Fail{field_316}:
1112	      Unit{}
1113	
1114	law Bq.ops_respect_requirements:
1115	  (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> (@+__2: Bq.WellEquipped(h_1) -> Bq.WellEquipped(Bq.hero_step(op_0, h_1)))))
1116	
1117	def Bq.ops_respect_requirements(op_0, h_1, __2):
1118	  match h_1:
1119	    case Bq.Hero.Hero{field_317, field_318, field_319, field_320, field_321, field_322, field_323, field_324, field_325, field_326, field_327}:
1120	      (apply_191 = {\{Bq.HOp.Equip: (k_0 => (inv_1 => (wea_2 => (arm_3 => (hel_4 => (chm_5 => (gold_6 => (lv_7 => (str_8 => (agi_9 => (vit_10 => (pts_11 => (apply_192 = {(k_0 => (wea_1 => (lv_2 => (str_3 => (agi_4 => (vit_5 => (arm_6 => (hel_7 => (chm_8 => (inv_9 => (gold_10 => (pts_11 => \{Bq.ISlot.SlotNone: (ei_12 => \{Tuple: (ww_13 => \{Tuple: (wa_14 => \{Tuple: (wh_15 => (wc_16 => Tuple{ww_13, Tuple{wa_14, Tuple{wh_15, wc_16}}})); \{}}); \{}}); \{}}); \{Bq.ISlot.SlotW: (ei_12 => (apply_193 = {(wea_0 => (lv_1 => (str_2 => (agi_3 => (vit_4 => (arm_5 => (hel_6 => (chm_7 => (k_8 => (inv_9 => (gold_10 => (pts_11 => (ei_12 => \{False: \{Tuple: (ww_13 => \{Tuple: (wa_14 => \{Tuple: (wh_15 => (wc_16 => Tuple{ww_13, Tuple{wa_14, Tuple{wh_15, wc_16}}})); \{}}); \{}}); \{}}; \{True: (apply_194 = {(lv_0 => (str_1 => (agi_2 => (vit_3 => (arm_4 => (hel_5 => (chm_6 => (k_7 => (inv_8 => (gold_9 => (pts_10 => (ei_11 => \{Done: (value_12 => \{Tuple: (ww_13 => \{Tuple: (wa_14 => \{Tuple: (wh_15 => (wc_16 => Tuple{ww_13, Tuple{wa_14, Tuple{wh_15, wc_16}}})); \{}}); \{}}); \{}}); \{Fail: (error_12 => (apply_195 = {(k_0 => (lv_1 => (str_2 => (agi_3 => (vit_4 => (arm_5 => (hel_6 => (chm_7 => (inv_8 => (error_9 => (gold_10 => (pts_11 => (ei_12 => \{False: (cw_13 => \{Tuple: (ww_14 => \{Tuple: (wa_15 => \{Tuple: (wh_16 => (wc_17 => Tuple{ww_14, Tuple{wa_15, Tuple{wh_16, wc_17}}})); \{}}); \{}}); \{}}); \{True: (cw_13 => \{Tuple: (ww_14 => \{Tuple: (wa_15 => \{Tuple: (wh_16 => (wc_17 => (%Equal.sym(Bq.ISlot, (apply_196 = {\{Bq.Info.Info: (slot_0 => (lvreq_1 => (streq_2 => (agireq_3 => (vitreq_4 => (atk_5 => (df_6 => (price_7 => slot_0)))))))); \{}} : (@+___0: Bq.Info -> Bq.ISlot)}; apply_196(Bq.item_info(k_0))), Bq.ISlot.SlotW{}, ei_12) : Bq.WellEquipped(({(inv_0 => (k_1 => (arm_2 => (hel_3 => (chm_4 => (gold_5 => (lv_6 => (str_7 => (agi_8 => (vit_9 => (pts_10 => (wea_11 => \{Bq.ISlot.SlotW: Bq.Hero.Hero{Bq.Bag.sub(inv_0, Bq.one(k_1)), Bq.Maybe.some(Nat, k_1), arm_2, hel_3, chm_4, gold_5
1121	
1122	law Bq.nmin_le_r:
1123	  (@+a_0: Nat -> (@+b_1: Nat -> {Bq.Nat.le(Bq.nmin(a_0, b_1), b_1) == True{} : Bool}))
1124	
1125	def Bq.nmin_le_r(a_0, b_1):
1126	  match a_0:
1127	    case Zero{}:
1128	      {==}
1129	    case Succ{field_328}:
1130	      match b_1:
1131	        case Zero{}:
1132	          {==}
1133	        case Succ{field_329}:
1134	          Bq.nmin_le_r(field_328, field_329)
1135	
1136	law Bq.damage_capped:
1137	  (@+watk_0: Nat -> (@+str_1: Nat -> (@+df_2: Nat -> (@+crit_3: Bool -> {Bq.Nat.le(Bq.damage(watk_0, str_1, df_2, crit_3), Bq.DMG_CAP) == True{} : Bool}))))
1138	
1139	def Bq.damage_capped(watk_0, str_1, df_2, crit_3):
1140	  Bq.nmin_le_r(Bq.nmax(Bq.Nat.sub(Bq.crit_dbl(crit_3, Bq.Nat.add(watk_0, Bq.Nat.dbl(str_1))), df_2), 1n), Bq.DMG_CAP)
1141	
1142	law Bq.nmin_pos:
1143	  (@+a_0: Nat -> (@+b_1: Nat -> (@+ea_2: {Bq.Nat.le(1n, a_0) == True{} : Bool} -> (@+eb_3: {Bq.Nat.le(1n, b_1) == True{} : Bool} -> {Bq.Nat.le(1n, Bq.nmin(a_0, b_1)) == True{} : Bool}))))
1144	
1145	def Bq.nmin_pos(a_0, b_1, ea_2, eb_3):
1146	  match a_0:
1147	    case Zero{}:
1148	      (apply_250 = {\{} : (@+___0: Empty -> {False{} == True{} : Bool})}; apply_250(Bq.Bool.false_ne_true(ea_2)))
1149	    case Succ{field_330}:
1150	      match b_1:
1151	        case Zero{}:
1152	          (apply_251 = {\{} : (@+___0: Empty -> {False{} == True{} : Bool})}; apply_251(Bq.Bool.false_ne_true(eb_3)))
1153	        case Succ{field_331}:
1154	          {==}
1155	
1156	law Bq.nmax_ge_one:
1157	  (@+x_0: Nat -> {Bq.Nat.le(1n, Bq.nmax(x_0, 1n)) == True{} : Bool})
1158	
1159	def Bq.nmax_ge_one(x_0):
1160	  match x_0:
1161	    case Zero{}:
1162	      {==}
1163	    case Succ{field_332}:
1164	      {==}
1165	
1166	law Bq.damage_at_least_one:
1167	  (@+watk_0: Nat -> (@+str_1: Nat -> (@+df_2: Nat -> (@+crit_3: Bool -> {Bq.Nat.le(1n, Bq.damage(watk_0, str_1, df_2, crit_3)) == True{} : Bool}))))
1168	
1169	def Bq.damage_at_least_one(watk_0, str_1, df_2, crit_3):
1170	  Bq.nmin_pos(Bq.nmax(Bq.Nat.sub(Bq.crit_dbl(crit_3, Bq.Nat.add(watk_0, Bq.Nat.dbl(str_1))), df_2), 1n), Bq.DMG_CAP, Bq.nmax_ge_one(Bq.Nat.sub(Bq.crit_dbl(crit_3, Bq.Nat.add(watk_0, Bq.Nat.dbl(str_1))), df_2)), {==})
1171	
1172	law Bq.le_nmax:
1173	  (@+a_0: Nat -> (@+b_1: Nat -> (@+c_2: Nat -> (@+ea_3: {Bq.Nat.le(a_0, c_2) == True{} : Bool} -> (@+eb_4: {Bq.Nat.le(b_1, c_2) == True{} : Bool} -> {Bq.Nat.le(Bq.nmax(a_0, b_1), c_2) == True{} : Bool})))))
1174	
1175	def Bq.le_nmax(a_0, b_1, c_2, ea_3, eb_4):
1176	  match a_0:
1177	    case Zero{}:
1178	      eb_4
1179	    case Succ{field_333}:
1180	      match b_1:
1181	        case Zero{}:
1182	          ea_3
1183	        case Succ{field_334}:
1184	          match c_2:
1185	            case Zero{}:
1186	              (apply_252 = {\{} : (@+___0: Empty -> {False{} == True{} : Bool})}; apply_252(Bq.Bool.false_ne_true(ea_3)))
1187	            case Succ{field_335}:
1188	              Bq.le_nmax(field_333, field_334, field_335, ea_3, eb_4)
1189	
1190	law Bq.no_instakill:
1191	  (@+matk_0: Nat -> (@+df_1: Nat -> (@+lv_2: Nat -> (@+vit_3: Nat -> {Bq.Nat.lt(Bq.mob_damage(matk_0, df_1, Bq.max_hp(lv_2, vit_3)), Bq.max_hp(lv_2, vit_3)) == True{} : Bool}))))
1192	
1193	def Bq.no_instakill(matk_0, df_1, lv_2, vit_3):
1194	  Bq.le_nmax(Bq.nmin(Bq.nmax(Bq.Nat.sub(matk_0, df_1), 1n), Bq.Nat.pred(Bq.max_hp(lv_2, vit_3))), 1n, Bq.Nat.pred(Bq.max_hp(lv_2, vit_3)), Bq.nmin_le_r(Bq.nmax(Bq.Nat.sub(matk_0, df_1), 1n), Bq.Nat.pred(Bq.max_hp(lv_2, vit_3))), {==})
1195	
1196	law Bq.le_step_down:
1197	  (@+a_0: Nat -> (@+b_1: Nat -> (@+e_2: {Bq.Nat.le(Succ{a_0}, b_1) == True{} : Bool} -> {Bq.Nat.le(a_0, b_1) == True{} : Bool})))
1198	
1199	def Bq.le_step_down(a_0, b_1, e_2):
1200	  match b_1:
1201	    case Zero{}:
1202	      (apply_253 = {(a_0 => \{}) : (@-a_0: Nat -> (@+___1: Empty -> {Bq.Nat.le(a_0, 0n) == True{} : Bool}))}; apply_253(a_0, Bq.Bool.false_ne_true(e_2)))
1203	    case Succ{field_336}:
1204	      Bq.le_succ_r(a_0, field_336, e_2)
1205	
1206	law Bq.walk_bounds_go:
1207	  (@+w_0: Nat -> (@+h_1: Nat -> (@+x_2: Nat -> (@+y_3: Nat -> (@+d_4: Bq.Dir -> (@+ex_5: {Bq.Nat.lt(x_2, w_0) == True{} : Bool} -> (@+ey_6: {Bq.Nat.lt(y_3, h_1) == True{} : Bool} -> {Bq.Bool.and(Bq.Nat.lt(Bq.walk_x(w_0, x_2, d_4), w_0), Bq.Nat.lt(Bq.walk_y(h_1, y_3, d_4), h_1)) == True{} : Bool})))))))
1208	
1209	def Bq.walk_bounds_go(w_0, h_1, x_2, y_3, d_4, ex_5, ey_6):
1210	  match d_4:
1211	    case Bq.Dir.DL{}:
1212	      (apply_254 = {(w_0 => (y_1 => (h_2 => \{Zero: (ex_3 => (ey_4 => Bq.and_intro(Bq.Nat.lt(0n, w_0), Bq.Nat.lt(y_1, h_2), ex_3, ey_4))); \{Succ: (p_3 => (ex_4 => (ey_5 => Bq.and_intro(Bq.Nat.lt(p_3, w_0), Bq.Nat.lt(y_1, h_2), Bq.le_step_down(Succ{p_3}, w_0, ex_4), ey_5)))); \{}}}))) : (@+w_0: Nat -> (@+y_1: Nat -> (@+h_2: Nat -> (@+___3: Nat -> (@+ex_4: {Bq.Nat.le(Succ{___3}, w_0) == True{} : Bool} -> (@+ey_5: {Bq.Nat.le(Succ{y_1}, h_2) == True{} : Bool} -> {Bq.Bool.and(Bq.Nat.le(Succ{Bq.Nat.pred(___3)}, w_0), Bq.Nat.le(Succ{y_1}, h_2)) == True{} : Bool}))))))}; apply_254(w_0, y_3, h_1, x_2, ex_5, ey_6))
1213	    case Bq.Dir.DR{}:
1214	      (apply_255 = {(x_0 => (w_1 => (y_2 => (h_3 => \{True: (t_4 => (ex_5 => (ey_6 => Bq.and_intro(Bq.Nat.lt(Succ{x_0}, w_1), Bq.Nat.lt(y_2, h_3), t_4, ey_6)))); \{False: (t_4 => (ex_5 => (ey_6 => Bq.and_intro(Bq.Nat.lt(x_0, w_1), Bq.Nat.lt(y_2, h_3), ex_5, ey_6)))); \{}}})))) : (@+x_0: Nat -> (@+w_1: Nat -> (@+y_2: Nat -> (@+h_3: Nat -> (@+___4: Bool -> (@+_e_5: {Bq.Nat.le(Succ{Succ{x_0}}, w_1) == ___4 : Bool} -> (@+ex_6: {Bq.Nat.le(Succ{x_0}, w_1) == True{} : Bool} -> (@+ey_7: {Bq.Nat.le(Succ{y_2}, h_3) == True{} : Bool} -> {Bq.Bool.and(Bq.Nat.le(Succ{(apply_256 = {(x_0 => \{True: Succ{x_0}; \{False: x_0; \{}}}) : (@+x_0: Nat -> (@+___1: Bool -> Nat))}; apply_256(x_0, ___4))}, w_1), Bq.Nat.le(Succ{y_2}, h_3)) == True{} : Bool}))))))))}; apply_255(x_2, w_0, y_3, h_1, Bq.Nat.lt(Succ{x_2}, w_0), {==}, ex_5, ey_6))
1215	    case Bq.Dir.DU{}:
1216	      (apply_257 = {(x_0 => (w_1 => (h_2 => \{Zero: (ex_3 => (ey_4 => Bq.and_intro(Bq.Nat.lt(x_0, w_1), Bq.Nat.lt(0n, h_2), ex_3, ey_4))); \{Succ: (p_3 => (ex_4 => (ey_5 => Bq.and_intro(Bq.Nat.lt(x_0, w_1), Bq.Nat.lt(p_3, h_2), ex_4, Bq.le_step_down(Succ{p_3}, h_2, ey_5))))); \{}}}))) : (@+x_0: Nat -> (@+w_1: Nat -> (@+h_2: Nat -> (@+___3: Nat -> (@+ex_4: {Bq.Nat.le(Succ{x_0}, w_1) == True{} : Bool} -> (@+ey_5: {Bq.Nat.le(Succ{___3}, h_2) == True{} : Bool} -> {Bq.Bool.and(Bq.Nat.le(Succ{x_0}, w_1), Bq.Nat.le(Succ{Bq.Nat.pred(___3)}, h_2)) == True{} : Bool}))))))}; apply_257(x_2, w_0, h_1, y_3, ex_5, ey_6))
1217	    case Bq.Dir.DD{}:
1218	      (apply_258 = {(y_0 => (h_1 => (x_2 => (w_3 => \{True: (t_4 => (ex_5 => (ey_6 => Bq.and_intro(Bq.Nat.lt(x_2, w_3), Bq.Nat.lt(Succ{y_0}, h_1), ex_5, t_4)))); \{False: (t_4 => (ex_5 => (ey_6 => Bq.and_intro(Bq.Nat.lt(x_2, w_3), Bq.Nat.lt(y_0, h_1), ex_5, ey_6)))); \{}}})))) : (@+y_0: Nat -> (@+h_1: Nat -> (@+x_2: Nat -> (@+w_3: Nat -> (@+___4: Bool -> (@+_e_5: {Bq.Nat.le(Succ{Succ{y_0}}, h_1) == ___4 : Bool} -> (@+ex_6: {Bq.Nat.le(Succ{x_2}, w_3) == True{} : Bool} -> (@+ey_7: {Bq.Nat.le(Succ{y_0}, h_1) == True{} : Bool} -> {Bq.Bool.and(Bq.Nat.le(Succ{x_2}, w_3), Bq.Nat.le(Succ{(apply_259 = {(y_0 => \{True: Succ{y_0}; \{False: y_0; \{}}}) : (@+y_0: Nat -> (@+___1: Bool -> Nat))}; apply_259(y_0, ___4))}, h_1)) == True{} : Bool}))))))))}; apply_258(y_3, h_1, x_2, w_0, Bq.Nat.lt(Succ{y_3}, h_1), {==}, ex_5, ey_6))
1219	
1220	law Bq.walk_stays_in_bounds:
1221	  (@+w_0: Nat -> (@+h_1: Nat -> (@+x_2: Nat -> (@+__3: {Bq.Nat.lt(x_2, w_0) == True{} : Bool} -> (@+y_4: Nat -> (@+__5: {Bq.Nat.lt(y_4, h_1) == True{} : Bool} -> (@+d_6: Bq.Dir -> {Bq.Bool.and(Bq.Nat.lt(Bq.walk_x(w_0, x_2, d_6), w_0), Bq.Nat.lt(Bq.walk_y(h_1, y_4, d_6), h_1)) == True{} : Bool})))))))
1222	
1223	def Bq.walk_stays_in_bounds(w_0, h_1, x_2, __3, y_4, __5, d_6):
1224	  Bq.walk_bounds_go(w_0, h_1, x_2, y_4, d_6, __3, __5)
1225	
1226	law Bq.Bool.or:
1227	  (@+a_0: Bool -> (@+b_1: Bool -> Bool))
1228	
1229	def Bq.Bool.or(a_0, b_1):
1230	  match a_0:
1231	    case True{}:
1232	      True{}
1233	    case False{}:
1234	      b_1
1235	
1236	law Bq.Nat.eq:
1237	  (@+a_0: Nat -> (@+b_1: Nat -> Bool))
1238	
1239	def Bq.Nat.eq(a_0, b_1):
1240	  match a_0:
1241	    case Zero{}:
1242	      match b_1:
1243	        case Zero{}:
1244	          True{}
1245	        case Succ{field_337}:
1246	          False{}
1247	    case Succ{field_338}:
1248	      match b_1:
1249	        case Zero{}:
1250	          False{}
1251	        case Succ{field_339}:
1252	          Bq.Nat.eq(field_338, field_339)
1253	
1254	law Bq.near:
1255	  (@+a_0: Nat -> (@+b_1: Nat -> Bool))
1256	
1257	def Bq.near(a_0, b_1):
1258	  Bq.Bool.or(Bq.Nat.eq(a_0, b_1), Bq.Bool.or(Bq.Nat.eq(Succ{a_0}, b_1), Bq.Nat.eq(a_0, Succ{b_1})))
1259	
1260	law Bq.Nat.eq_refl:
1261	  (@+a_0: Nat -> {Bq.Nat.eq(a_0, a_0) == True{} : Bool})
1262	
1263	def Bq.Nat.eq_refl(a_0):
1264	  match a_0:
1265	    case Zero{}:
1266	      {==}
1267	    case Succ{field_340}:
1268	      Bq.Nat.eq_refl(field_340)
1269	
1270	law Bq.near_self:
1271	  (@+x_0: Nat -> {Bq.near(x_0, x_0) == True{} : Bool})
1272	
1273	def Bq.near_self(x_0):
1274	  (%Equal.sym(Bool, Bq.Nat.eq(x_0, x_0), True{}, Bq.Nat.eq_refl(x_0)) : {Bq.Bool.or(_, Bq.Bool.or(Bq.Nat.eq(Succ{x_0}, x_0), Bq.Nat.eq(x_0, Succ{x_0}))) == True{} : Bool}; {==})
1275	
1276	law Bq.neq_succ:
1277	  (@+x_0: Nat -> {Bq.Nat.eq(Succ{x_0}, x_0) == False{} : Bool})
1278	
1279	def Bq.neq_succ(x_0):
1280	  match x_0:
1281	    case Zero{}:
1282	      {==}
1283	    case Succ{field_341}:
1284	      Bq.neq_succ(field_341)
1285	
1286	law Bq.neq_succ2:
1287	  (@+x_0: Nat -> {Bq.Nat.eq(Succ{Succ{x_0}}, x_0) == False{} : Bool})
1288	
1289	def Bq.neq_succ2(x_0):
1290	  match x_0:
1291	    case Zero{}:
1292	      {==}
1293	    case Succ{field_342}:
1294	      Bq.neq_succ2(field_342)
1295	
1296	law Bq.near_pred:
1297	  (@+x_0: Nat -> {Bq.near(x_0, Bq.Nat.pred(x_0)) == True{} : Bool})
1298	
1299	def Bq.near_pred(x_0):
1300	  match x_0:
1301	    case Zero{}:
1302	      {==}
1303	    case Succ{field_343}:
1304	      (%Equal.sym(Bool, Bq.Nat.eq(Succ{field_343}, field_343), False{}, Bq.neq_succ(field_343)) : {Bq.Bool.or(_, Bq.Bool.or(Bq.Nat.eq(Succ{Succ{field_343}}, field_343), Bq.Nat.eq(field_343, field_343))) == True{} : Bool}; (%Equal.sym(Bool, Bq.Nat.eq(Succ{Succ{field_343}}, field_343), False{}, Bq.neq_succ2(field_343)) : {Bq.Bool.or(_, Bq.Nat.eq(field_343, field_343)) == True{} : Bool}; (%Equal.sym(Bool, Bq.Nat.eq(field_343, field_343), True{}, Bq.Nat.eq_refl(field_343)) : {_ == True{} : Bool}; {==})))
1305	
1306	law Bq.neq_succ_r:
1307	  (@+x_0: Nat -> {Bq.Nat.eq(x_0, Succ{x_0}) == False{} : Bool})
1308	
1309	def Bq.neq_succ_r(x_0):
1310	  match x_0:
1311	    case Zero{}:
1312	      {==}
1313	    case Succ{field_344}:
1314	      Bq.neq_succ_r(field_344)
1315	
1316	law Bq.near_succ:
1317	  (@+x_0: Nat -> {Bq.near(x_0, Succ{x_0}) == True{} : Bool})
1318	
1319	def Bq.near_succ(x_0):
1320	  (%Equal.sym(Bool, Bq.Nat.eq(x_0, Succ{x_0}), False{}, Bq.neq_succ_r(x_0)) : {Bq.Bool.or(_, Bq.Bool.or(Bq.Nat.eq(x_0, x_0), Bq.Nat.eq(x_0, Succ{Succ{x_0}}))) == True{} : Bool}; (%Equal.sym(Bool, Bq.Nat.eq(x_0, x_0), True{}, Bq.Nat.eq_refl(x_0)) : {Bq.Bool.or(_, Bq.Nat.eq(x_0, Succ{Succ{x_0}})) == True{} : Bool}; {==}))
1321	
1322	law Bq.walk_is_adjacent:
1323	  (@+w_0: Nat -> (@+h_1: Nat -> (@+x_2: Nat -> (@+y_3: Nat -> (@+d_4: Bq.Dir -> {Bq.Bool.and(Bq.near(x_2, Bq.walk_x(w_0, x_2, d_4)), Bq.near(y_3, Bq.walk_y(h_1, y_3, d_4))) == True{} : Bool})))))
1324	
1325	def Bq.walk_is_adjacent(w_0, h_1, x_2, y_3, d_4):
1326	  match d_4:
1327	    case Bq.Dir.DU{}:
1328	      Bq.and_intro(Bq.near(x_2, x_2), Bq.near(y_3, Bq.Nat.pred(y_3)), Bq.near_self(x_2), Bq.near_pred(y_3))
1329	    case Bq.Dir.DD{}:
1330	      (apply_260 = {(x_0 => (y_1 => \{True: Bq.and_intro(Bq.near(x_0, x_0), Bq.near(y_1, Succ{y_1}), Bq.near_self(x_0), Bq.near_succ(y_1)); \{False: Bq.and_intro(Bq.near(x_0, x_0), Bq.near(y_1, y_1), Bq.near_self(x_0), Bq.near_self(y_1)); \{}}})) : (@+x_0: Nat -> (@+y_1: Nat -> (@+___2: Bool -> {Bq.Bool.and(Bq.Bool.or(Bq.Nat.eq(x_0, x_0), Bq.Bool.or(Bq.Nat.eq(Succ{x_0}, x_0), Bq.Nat.eq(x_0, Succ{x_0}))), Bq.Bool.or(Bq.Nat.eq(y_1, (apply_261 = {(y_0 => \{True: Succ{y_0}; \{False: y_0; \{}}}) : (@+y_0: Nat -> (@+___1: Bool -> Nat))}; apply_261(y_1, ___2))), Bq.Bool.or(Bq.Nat.eq(Succ{y_1}, (apply_262 = {(y_0 => \{True: Succ{y_0}; \{False: y_0; \{}}}) : (@+y_0: Nat -> (@+___1: Bool -> Nat))}; apply_262(y_1, ___2))), Bq.Nat.eq(y_1, Succ{(apply_263 = {(y_0 => \{True: Succ{y_0}; \{False: y_0; \{}}}) : (@+y_0: Nat -> (@+___1: Bool -> Nat))}; apply_263(y_1, ___2))})))) == True{} : Bool})))}; apply_260(x_2, y_3, Bq.Nat.lt(Succ{y_3}, h_1)))
1331	    case Bq.Dir.DL{}:
1332	      Bq.and_intro(Bq.near(x_2, Bq.Nat.pred(x_2)), Bq.near(y_3, y_3), Bq.near_pred(x_2), Bq.near_self(y_3))
1333	    case Bq.Dir.DR{}:
1334	      (apply_264 = {(x_0 => (y_1 => \{True: Bq.and_intro(Bq.near(x_0, Succ{x_0}), Bq.near(y_1, y_1), Bq.near_succ(x_0), Bq.near_self(y_1)); \{False: Bq.and_intro(Bq.near(x_0, x_0), Bq.near(y_1, y_1), Bq.near_self(x_0), Bq.near_self(y_1)); \{}}})) : (@+x_0: Nat -> (@+y_1: Nat -> (@+___2: Bool -> {Bq.Bool.and(Bq.Bool.or(Bq.Nat.eq(x_0, (apply_265 = {(x_0 => \{True: Succ{x_0}; \{False: x_0; \{}}}) : (@+x_0: Nat -> (@+___1: Bool -> Nat))}; apply_265(x_0, ___2))), Bq.Bool.or(Bq.Nat.eq(Succ{x_0}, (apply_266 = {(x_0 => \{True: Succ{x_0}; \{False: x_0; \{}}}) : (@+x_0: Nat -> (@+___1: Bool -> Nat))}; apply_266(x_0, ___2))), Bq.Nat.eq(x_0, Succ{(apply_267 = {(x_0 => \{True: Succ{x_0}; \{False: x_0; \{}}}) : (@+x_0: Nat -> (@+___1: Bool -> Nat))}; apply_267(x_0, ___2))}))), Bq.Bool.or(Bq.Nat.eq(y_1, y_1), Bq.Bool.or(Bq.Nat.eq(Succ{y_1}, y_1), Bq.Nat.eq(y_1, Succ{y_1})))) == True{} : Bool})))}; apply_264(x_2, y_3, Bq.Nat.lt(Succ{x_2}, w_0)))