def aria_sb24
import bend-osdev-aria@0.1.0.0/PROOF.bend as PROOFimport Base
import bend-osdev-aria@0.1.0.0/aria.bend as A
4620def aria_sb24(w0: Word(8n)) -> {w0 == A.aria.sb2(A.aria.sb4(w0)) : Word(8n)}:
4621 match w0:
4622 case WCon{False{}, w1}:
4623 match w1:
4624 case WCon{False{}, w2}:
4625 match w2:
4626 case WCon{False{}, w3}:
4627 match w3:
4628 case WCon{False{}, w4}:
4629 match w4:
4630 case WCon{False{}, w5}:
4631 match w5:
4632 case WCon{False{}, w6}:
4633 match w6:
4634 case WCon{False{}, w7}:
4635 match w7:
4636 case WCon{False{}, w8}:
4637 match w8:
4638 case WNil{}:
4639 {==}
4640 case WCon{True{}, w8}:
4641 match w8:
4642 case WNil{}:
4643 {==}
4644 case WCon{True{}, w7}:
4645 match w7:
4646 case WCon{False{}, w8}:
4647 match w8:
4648 case WNil{}:
4649 {==}
4650 case WCon{True{}, w8}:
4651 match w8:
4652 case WNil{}:
4653 {==}
4654 case WCon{True{}, w6}:
4655 match w6:
4656 case WCon{False{}, w7}:
4657 match w7:
4658 case WCon{False{}, w8}:
4659 match w8:
4660 case WNil{}:
4661 {==}
4662 case WCon{True{}, w8}:
4663 match w8:
4664 case WNil{}:
4665 {==}
4666 case WCon{True{}, w7}:
4667 match w7:
4668 case WCon{False{}, w8}:
4669 match w8:
4670 case WNil{}:
4671 {==}
4672 case WCon{True{}, w8}:
4673 match w8:
4674 case WNil{}:
4675 {==}
4676 case WCon{True{}, w5}:
4677 match w5:
4678 case WCon{False{}, w6}:
4679 match w6:
4680 case WCon{False{}, w7}:
4681 match w7:
4682 case WCon{False{}, w8}:
4683 match w8:
4684 case WNil{}:
4685 {==}
4686 case WCon{True{}, w8}:
4687 match w8:
4688 case WNil{}:
4689 {==}
4690 case WCon{True{}, w7}:
4691 match w7:
4692 case WCon{False{}, w8}:
4693 match w8:
4694 case WNil{}:
4695 {==}
4696 case WCon{True{}, w8}:
4697 match w8:
4698 case WNil{}:
4699 {==}
4700 case WCon{True{}, w6}:
4701 match w6:
4702 case WCon{False{}, w7}:
4703 match w7:
4704 case WCon{False{}, w8}:
4705 match w8:
4706 case WNil{}:
4707 {==}
4708 case WCon{True{}, w8}:
4709 match w8:
4710 case WNil{}:
4711 {==}
4712 case WCon{True{}, w7}:
4713 match w7:
4714 case WCon{False{}, w8}:
4715 match w8:
4716 case WNil{}:
4717 {==}
4718 case WCon{True{}, w8}:
4719 match w8:
4720 case WNil{}:
4721 {==}
4722 case WCon{True{}, w4}:
4723 match w4:
4724 case WCon{False{}, w5}:
4725 match w5:
4726 case WCon{False{}, w6}:
4727 match w6:
4728 case WCon{False{}, w7}:
4729 match w7:
4730 case WCon{False{}, w8}:
4731 match w8:
4732 case WNil{}:
4733 {==}
4734 case WCon{True{}, w8}:
4735 match w8:
4736 case WNil{}:
4737 {==}
4738 case WCon{True{}, w7}:
4739 match w7:
4740 case WCon{False{}, w8}:
4741 match w8:
4742 case WNil{}:
4743 {==}
4744 case WCon{True{}, w8}:
4745 match w8:
4746 case WNil{}:
4747 {==}
4748 case WCon{True{}, w6}:
4749 match w6:
4750 case WCon{False{}, w7}:
4751 match w7:
4752 case WCon{False{}, w8}:
4753 match w8:
4754 case WNil{}:
4755 {==}
4756 case WCon{True{}, w8}:
4757 match w8:
4758 case WNil{}:
4759 {==}
4760 case WCon{True{}, w7}:
4761 match w7:
4762 case WCon{False{}, w8}:
4763 match w8:
4764 case WNil{}:
4765 {==}
4766 case WCon{True{}, w8}:
4767 match w8:
4768 case WNil{}:
4769 {==}
4770 case WCon{True{}, w5}:
4771 match w5:
4772 case WCon{False{}, w6}:
4773 match w6:
4774 case WCon{False{}, w7}:
4775 match w7:
4776 case WCon{False{}, w8}:
4777 match w8:
4778 case WNil{}:
4779 {==}
4780 case WCon{True{}, w8}:
4781 match w8:
4782 case WNil{}:
4783 {==}
4784 case WCon{True{}, w7}:
4785 match w7:
4786 case WCon{False{}, w8}:
4787 match w8:
4788 case WNil{}:
4789 {==}
4790 case WCon{True{}, w8}:
4791 match w8:
4792 case WNil{}:
4793 {==}
4794 case WCon{True{}, w6}:
4795 match w6:
4796 case WCon{False{}, w7}:
4797 match w7:
4798 case WCon{False{}, w8}:
4799 match w8:
4800 case WNil{}:
4801 {==}
4802 case WCon{True{}, w8}:
4803 match w8:
4804 case WNil{}:
4805 {==}
4806 case WCon{True{}, w7}:
4807 match w7:
4808 case WCon{False{}, w8}:
4809 match w8:
4810 case WNil{}:
4811 {==}
4812 case WCon{True{}, w8}:
4813 match w8:
4814 case WNil{}:
4815 {==}
4816 case WCon{True{}, w3}:
4817 match w3:
4818 case WCon{False{}, w4}:
4819 match w4:
4820 case WCon{False{}, w5}:
4821 match w5:
4822 case WCon{False{}, w6}:
4823 match w6:
4824 case WCon{False{}, w7}:
4825 match w7:
4826 case WCon{False{}, w8}:
4827 match w8:
4828 case WNil{}:
4829 {==}
4830 case WCon{True{}, w8}:
4831 match w8:
4832 case WNil{}:
4833 {==}
4834 case WCon{True{}, w7}:
4835 match w7:
4836 case WCon{False{}, w8}:
4837 match w8:
4838 case WNil{}:
4839 {==}
4840 case WCon{True{}, w8}:
4841 match w8:
4842 case WNil{}:
4843 {==}
4844 case WCon{True{}, w6}:
4845 match w6:
4846 case WCon{False{}, w7}:
4847 match w7:
4848 case WCon{False{}, w8}:
4849 match w8:
4850 case WNil{}:
4851 {==}
4852 case WCon{True{}, w8}:
4853 match w8:
4854 case WNil{}:
4855 {==}
4856 case WCon{True{}, w7}:
4857 match w7:
4858 case WCon{False{}, w8}:
4859 match w8:
4860 case WNil{}:
4861 {==}
4862 case WCon{True{}, w8}:
4863 match w8:
4864 case WNil{}:
4865 {==}
4866 case WCon{True{}, w5}:
4867 match w5:
4868 case WCon{False{}, w6}:
4869 match w6:
4870 case WCon{False{}, w7}:
4871 match w7:
4872 case WCon{False{}, w8}:
4873 match w8:
4874 case WNil{}:
4875 {==}
4876 case WCon{True{}, w8}:
4877 match w8:
4878 case WNil{}:
4879 {==}
4880 case WCon{True{}, w7}:
4881 match w7:
4882 case WCon{False{}, w8}:
4883 match w8:
4884 case WNil{}:
4885 {==}
4886 case WCon{True{}, w8}:
4887 match w8:
4888 case WNil{}:
4889 {==}
4890 case WCon{True{}, w6}:
4891 match w6:
4892 case WCon{False{}, w7}:
4893 match w7:
4894 case WCon{False{}, w8}:
4895 match w8:
4896 case WNil{}:
4897 {==}
4898 case WCon{True{}, w8}:
4899 match w8:
4900 case WNil{}:
4901 {==}
4902 case WCon{True{}, w7}:
4903 match w7:
4904 case WCon{False{}, w8}:
4905 match w8:
4906 case WNil{}:
4907 {==}
4908 case WCon{True{}, w8}:
4909 match w8:
4910 case WNil{}:
4911 {==}
4912 case WCon{True{}, w4}:
4913 match w4:
4914 case WCon{False{}, w5}:
4915 match w5:
4916 case WCon{False{}, w6}:
4917 match w6:
4918 case WCon{False{}, w7}:
4919 match w7:
4920 case WCon{False{}, w8}:
4921 match w8:
4922 case WNil{}:
4923 {==}
4924 case WCon{True{}, w8}:
4925 match w8:
4926 case WNil{}:
4927 {==}
4928 case WCon{True{}, w7}:
4929 match w7:
4930 case WCon{False{}, w8}:
4931 match w8:
4932 case WNil{}:
4933 {==}
4934 case WCon{True{}, w8}:
4935 match w8:
4936 case WNil{}:
4937 {==}
4938 case WCon{True{}, w6}:
4939 match w6:
4940 case WCon{False{}, w7}:
4941 match w7:
4942 case WCon{False{}, w8}:
4943 match w8:
4944 case WNil{}:
4945 {==}
4946 case WCon{True{}, w8}:
4947 match w8:
4948 case WNil{}:
4949 {==}
4950 case WCon{True{}, w7}:
4951 match w7:
4952 case WCon{False{}, w8}:
4953 match w8:
4954 case WNil{}:
4955 {==}
4956 case WCon{True{}, w8}:
4957 match w8:
4958 case WNil{}:
4959 {==}
4960 case WCon{True{}, w5}:
4961 match w5:
4962 case WCon{False{}, w6}:
4963 match w6:
4964 case WCon{False{}, w7}:
4965 match w7:
4966 case WCon{False{}, w8}:
4967 match w8:
4968 case WNil{}:
4969 {==}
4970 case WCon{True{}, w8}:
4971 match w8:
4972 case WNil{}:
4973 {==}
4974 case WCon{True{}, w7}:
4975 match w7:
4976 case WCon{False{}, w8}:
4977 match w8:
4978 case WNil{}:
4979 {==}
4980 case WCon{True{}, w8}:
4981 match w8:
4982 case WNil{}:
4983 {==}
4984 case WCon{True{}, w6}:
4985 match w6:
4986 case WCon{False{}, w7}:
4987 match w7:
4988 case WCon{False{}, w8}:
4989 match w8:
4990 case WNil{}:
4991 {==}
4992 case WCon{True{}, w8}:
4993 match w8:
4994 case WNil{}:
4995 {==}
4996 case WCon{True{}, w7}:
4997 match w7:
4998 case WCon{False{}, w8}:
4999 match w8:
5000 case WNil{}:
5001 {==}
5002 case WCon{True{}, w8}:
5003 match w8:
5004 case WNil{}:
5005 {==}
5006 case WCon{True{}, w2}:
5007 match w2:
5008 case WCon{False{}, w3}:
5009 match w3:
5010 case WCon{False{}, w4}:
5011 match w4:
5012 case WCon{False{}, w5}:
5013 match w5:
5014 case WCon{False{}, w6}:
5015 match w6:
5016 case WCon{False{}, w7}:
5017 match w7:
5018 case WCon{False{}, w8}:
5019 match w8:
5020 case WNil{}:
5021 {==}
5022 case WCon{True{}, w8}:
5023 match w8:
5024 case WNil{}:
5025 {==}
5026 case WCon{True{}, w7}:
5027 match w7:
5028 case WCon{False{}, w8}:
5029 match w8:
5030 case WNil{}:
5031 {==}
5032 case WCon{True{}, w8}:
5033 match w8:
5034 case WNil{}:
5035 {==}
5036 case WCon{True{}, w6}:
5037 match w6:
5038 case WCon{False{}, w7}:
5039 match w7:
5040 case WCon{False{}, w8}:
5041 match w8:
5042 case WNil{}:
5043 {==}
5044 case WCon{True{}, w8}:
5045 match w8:
5046 case WNil{}:
5047 {==}
5048 case WCon{True{}, w7}:
5049 match w7:
5050 case WCon{False{}, w8}:
5051 match w8:
5052 case WNil{}:
5053 {==}
5054 case WCon{True{}, w8}:
5055 match w8:
5056 case WNil{}:
5057 {==}
5058 case WCon{True{}, w5}:
5059 match w5:
5060 case WCon{False{}, w6}:
5061 match w6:
5062 case WCon{False{}, w7}:
5063 match w7:
5064 case WCon{False{}, w8}:
5065 match w8:
5066 case WNil{}:
5067 {==}
5068 case WCon{True{}, w8}:
5069 match w8:
5070 case WNil{}:
5071 {==}
5072 case WCon{True{}, w7}:
5073 match w7:
5074 case WCon{False{}, w8}:
5075 match w8:
5076 case WNil{}:
5077 {==}
5078 case WCon{True{}, w8}:
5079 match w8:
5080 case WNil{}:
5081 {==}
5082 case WCon{True{}, w6}:
5083 match w6:
5084 case WCon{False{}, w7}:
5085 match w7:
5086 case WCon{False{}, w8}:
5087 match w8:
5088 case WNil{}:
5089 {==}
5090 case WCon{True{}, w8}:
5091 match w8:
5092 case WNil{}:
5093 {==}
5094 case WCon{True{}, w7}:
5095 match w7:
5096 case WCon{False{}, w8}:
5097 match w8:
5098 case WNil{}:
5099 {==}
5100 case WCon{True{}, w8}:
5101 match w8:
5102 case WNil{}:
5103 {==}
5104 case WCon{True{}, w4}:
5105 match w4:
5106 case WCon{False{}, w5}:
5107 match w5:
5108 case WCon{False{}, w6}:
5109 match w6:
5110 case WCon{False{}, w7}:
5111 match w7:
5112 case WCon{False{}, w8}:
5113 match w8:
5114 case WNil{}:
5115 {==}
5116 case WCon{True{}, w8}:
5117 match w8:
5118 case WNil{}:
5119 {==}
5120 case WCon{True{}, w7}:
5121 match w7:
5122 case WCon{False{}, w8}:
5123 match w8:
5124 case WNil{}:
5125 {==}
5126 case WCon{True{}, w8}:
5127 match w8:
5128 case WNil{}:
5129 {==}
5130 case WCon{True{}, w6}:
5131 match w6:
5132 case WCon{False{}, w7}:
5133 match w7:
5134 case WCon{False{}, w8}:
5135 match w8:
5136 case WNil{}:
5137 {==}
5138 case WCon{True{}, w8}:
5139 match w8:
5140 case WNil{}:
5141 {==}
5142 case WCon{True{}, w7}:
5143 match w7:
5144 case WCon{False{}, w8}:
5145 match w8:
5146 case WNil{}:
5147 {==}
5148 case WCon{True{}, w8}:
5149 match w8:
5150 case WNil{}:
5151 {==}
5152 case WCon{True{}, w5}:
5153 match w5:
5154 case WCon{False{}, w6}:
5155 match w6:
5156 case WCon{False{}, w7}:
5157 match w7:
5158 case WCon{False{}, w8}:
5159 match w8:
5160 case WNil{}:
5161 {==}
5162 case WCon{True{}, w8}:
5163 match w8:
5164 case WNil{}:
5165 {==}
5166 case WCon{True{}, w7}:
5167 match w7:
5168 case WCon{False{}, w8}:
5169 match w8:
5170 case WNil{}:
5171 {==}
5172 case WCon{True{}, w8}:
5173 match w8:
5174 case WNil{}:
5175 {==}
5176 case WCon{True{}, w6}:
5177 match w6:
5178 case WCon{False{}, w7}:
5179 match w7:
5180 case WCon{False{}, w8}:
5181 match w8:
5182 case WNil{}:
5183 {==}
5184 case WCon{True{}, w8}:
5185 match w8:
5186 case WNil{}:
5187 {==}
5188 case WCon{True{}, w7}:
5189 match w7:
5190 case WCon{False{}, w8}:
5191 match w8:
5192 case WNil{}:
5193 {==}
5194 case WCon{True{}, w8}:
5195 match w8:
5196 case WNil{}:
5197 {==}
5198 case WCon{True{}, w3}:
5199 match w3:
5200 case WCon{False{}, w4}:
5201 match w4:
5202 case WCon{False{}, w5}:
5203 match w5:
5204 case WCon{False{}, w6}:
5205 match w6:
5206 case WCon{False{}, w7}:
5207 match w7:
5208 case WCon{False{}, w8}:
5209 match w8:
5210 case WNil{}:
5211 {==}
5212 case WCon{True{}, w8}:
5213 match w8:
5214 case WNil{}:
5215 {==}
5216 case WCon{True{}, w7}:
5217 match w7:
5218 case WCon{False{}, w8}:
5219 match w8:
5220 case WNil{}:
5221 {==}
5222 case WCon{True{}, w8}:
5223 match w8:
5224 case WNil{}:
5225 {==}
5226 case WCon{True{}, w6}:
5227 match w6:
5228 case WCon{False{}, w7}:
5229 match w7:
5230 case WCon{False{}, w8}:
5231 match w8:
5232 case WNil{}:
5233 {==}
5234 case WCon{True{}, w8}:
5235 match w8:
5236 case WNil{}:
5237 {==}
5238 case WCon{True{}, w7}:
5239 match w7:
5240 case WCon{False{}, w8}:
5241 match w8:
5242 case WNil{}:
5243 {==}
5244 case WCon{True{}, w8}:
5245 match w8:
5246 case WNil{}:
5247 {==}
5248 case WCon{True{}, w5}:
5249 match w5:
5250 case WCon{False{}, w6}:
5251 match w6:
5252 case WCon{False{}, w7}:
5253 match w7:
5254 case WCon{False{}, w8}:
5255 match w8:
5256 case WNil{}:
5257 {==}
5258 case WCon{True{}, w8}:
5259 match w8:
5260 case WNil{}:
5261 {==}
5262 case WCon{True{}, w7}:
5263 match w7:
5264 case WCon{False{}, w8}:
5265 match w8:
5266 case WNil{}:
5267 {==}
5268 case WCon{True{}, w8}:
5269 match w8:
5270 case WNil{}:
5271 {==}
5272 case WCon{True{}, w6}:
5273 match w6:
5274 case WCon{False{}, w7}:
5275 match w7:
5276 case WCon{False{}, w8}:
5277 match w8:
5278 case WNil{}:
5279 {==}
5280 case WCon{True{}, w8}:
5281 match w8:
5282 case WNil{}:
5283 {==}
5284 case WCon{True{}, w7}:
5285 match w7:
5286 case WCon{False{}, w8}:
5287 match w8:
5288 case WNil{}:
5289 {==}
5290 case WCon{True{}, w8}:
5291 match w8:
5292 case WNil{}:
5293 {==}
5294 case WCon{True{}, w4}:
5295 match w4:
5296 case WCon{False{}, w5}:
5297 match w5:
5298 case WCon{False{}, w6}:
5299 match w6:
5300 case WCon{False{}, w7}:
5301 match w7:
5302 case WCon{False{}, w8}:
5303 match w8:
5304 case WNil{}:
5305 {==}
5306 case WCon{True{}, w8}:
5307 match w8:
5308 case WNil{}:
5309 {==}
5310 case WCon{True{}, w7}:
5311 match w7:
5312 case WCon{False{}, w8}:
5313 match w8:
5314 case WNil{}:
5315 {==}
5316 case WCon{True{}, w8}:
5317 match w8:
5318 case WNil{}:
5319 {==}
5320 case WCon{True{}, w6}:
5321 match w6:
5322 case WCon{False{}, w7}:
5323 match w7:
5324 case WCon{False{}, w8}:
5325 match w8:
5326 case WNil{}:
5327 {==}
5328 case WCon{True{}, w8}:
5329 match w8:
5330 case WNil{}:
5331 {==}
5332 case WCon{True{}, w7}:
5333 match w7:
5334 case WCon{False{}, w8}:
5335 match w8:
5336 case WNil{}:
5337 {==}
5338 case WCon{True{}, w8}:
5339 match w8:
5340 case WNil{}:
5341 {==}
5342 case WCon{True{}, w5}:
5343 match w5:
5344 case WCon{False{}, w6}:
5345 match w6:
5346 case WCon{False{}, w7}:
5347 match w7:
5348 case WCon{False{}, w8}:
5349 match w8:
5350 case WNil{}:
5351 {==}
5352 case WCon{True{}, w8}:
5353 match w8:
5354 case WNil{}:
5355 {==}
5356 case WCon{True{}, w7}:
5357 match w7:
5358 case WCon{False{}, w8}:
5359 match w8:
5360 case WNil{}:
5361 {==}
5362 case WCon{True{}, w8}:
5363 match w8:
5364 case WNil{}:
5365 {==}
5366 case WCon{True{}, w6}:
5367 match w6:
5368 case WCon{False{}, w7}:
5369 match w7:
5370 case WCon{False{}, w8}:
5371 match w8:
5372 case WNil{}:
5373 {==}
5374 case WCon{True{}, w8}:
5375 match w8:
5376 case WNil{}:
5377 {==}
5378 case WCon{True{}, w7}:
5379 match w7:
5380 case WCon{False{}, w8}:
5381 match w8:
5382 case WNil{}:
5383 {==}
5384 case WCon{True{}, w8}:
5385 match w8:
5386 case WNil{}:
5387 {==}
5388 case WCon{True{}, w1}:
5389 match w1:
5390 case WCon{False{}, w2}:
5391 match w2:
5392 case WCon{False{}, w3}:
5393 match w3:
5394 case WCon{False{}, w4}:
5395 match w4:
5396 case WCon{False{}, w5}:
5397 match w5:
5398 case WCon{False{}, w6}:
5399 match w6:
5400 case WCon{False{}, w7}:
5401 match w7:
5402 case WCon{False{}, w8}:
5403 match w8:
5404 case WNil{}:
5405 {==}
5406 case WCon{True{}, w8}:
5407 match w8:
5408 case WNil{}:
5409 {==}
5410 case WCon{True{}, w7}:
5411 match w7:
5412 case WCon{False{}, w8}:
5413 match w8:
5414 case WNil{}:
5415 {==}
5416 case WCon{True{}, w8}:
5417 match w8:
5418 case WNil{}:
5419 {==}
5420 case WCon{True{}, w6}:
5421 match w6:
5422 case WCon{False{}, w7}:
5423 match w7:
5424 case WCon{False{}, w8}:
5425 match w8:
5426 case WNil{}:
5427 {==}
5428 case WCon{True{}, w8}:
5429 match w8:
5430 case WNil{}:
5431 {==}
5432 case WCon{True{}, w7}:
5433 match w7:
5434 case WCon{False{}, w8}:
5435 match w8:
5436 case WNil{}:
5437 {==}
5438 case WCon{True{}, w8}:
5439 match w8:
5440 case WNil{}:
5441 {==}
5442 case WCon{True{}, w5}:
5443 match w5:
5444 case WCon{False{}, w6}:
5445 match w6:
5446 case WCon{False{}, w7}:
5447 match w7:
5448 case WCon{False{}, w8}:
5449 match w8:
5450 case WNil{}:
5451 {==}
5452 case WCon{True{}, w8}:
5453 match w8:
5454 case WNil{}:
5455 {==}
5456 case WCon{True{}, w7}:
5457 match w7:
5458 case WCon{False{}, w8}:
5459 match w8:
5460 case WNil{}:
5461 {==}
5462 case WCon{True{}, w8}:
5463 match w8:
5464 case WNil{}:
5465 {==}
5466 case WCon{True{}, w6}:
5467 match w6:
5468 case WCon{False{}, w7}:
5469 match w7:
5470 case WCon{False{}, w8}:
5471 match w8:
5472 case WNil{}:
5473 {==}
5474 case WCon{True{}, w8}:
5475 match w8:
5476 case WNil{}:
5477 {==}
5478 case WCon{True{}, w7}:
5479 match w7:
5480 case WCon{False{}, w8}:
5481 match w8:
5482 case WNil{}:
5483 {==}
5484 case WCon{True{}, w8}:
5485 match w8:
5486 case WNil{}:
5487 {==}
5488 case WCon{True{}, w4}:
5489 match w4:
5490 case WCon{False{}, w5}:
5491 match w5:
5492 case WCon{False{}, w6}:
5493 match w6:
5494 case WCon{False{}, w7}:
5495 match w7:
5496 case WCon{False{}, w8}:
5497 match w8:
5498 case WNil{}:
5499 {==}
5500 case WCon{True{}, w8}:
5501 match w8:
5502 case WNil{}:
5503 {==}
5504 case WCon{True{}, w7}:
5505 match w7:
5506 case WCon{False{}, w8}:
5507 match w8:
5508 case WNil{}:
5509 {==}
5510 case WCon{True{}, w8}:
5511 match w8:
5512 case WNil{}:
5513 {==}
5514 case WCon{True{}, w6}:
5515 match w6:
5516 case WCon{False{}, w7}:
5517 match w7:
5518 case WCon{False{}, w8}:
5519 match w8:
5520 case WNil{}:
5521 {==}
5522 case WCon{True{}, w8}:
5523 match w8:
5524 case WNil{}:
5525 {==}
5526 case WCon{True{}, w7}:
5527 match w7:
5528 case WCon{False{}, w8}:
5529 match w8:
5530 case WNil{}:
5531 {==}
5532 case WCon{True{}, w8}:
5533 match w8:
5534 case WNil{}:
5535 {==}
5536 case WCon{True{}, w5}:
5537 match w5:
5538 case WCon{False{}, w6}:
5539 match w6:
5540 case WCon{False{}, w7}:
5541 match w7:
5542 case WCon{False{}, w8}:
5543 match w8:
5544 case WNil{}:
5545 {==}
5546 case WCon{True{}, w8}:
5547 match w8:
5548 case WNil{}:
5549 {==}
5550 case WCon{True{}, w7}:
5551 match w7:
5552 case WCon{False{}, w8}:
5553 match w8:
5554 case WNil{}:
5555 {==}
5556 case WCon{True{}, w8}:
5557 match w8:
5558 case WNil{}:
5559 {==}
5560 case WCon{True{}, w6}:
5561 match w6:
5562 case WCon{False{}, w7}:
5563 match w7:
5564 case WCon{False{}, w8}:
5565 match w8:
5566 case WNil{}:
5567 {==}
5568 case WCon{True{}, w8}:
5569 match w8:
5570 case WNil{}:
5571 {==}
5572 case WCon{True{}, w7}:
5573 match w7:
5574 case WCon{False{}, w8}:
5575 match w8:
5576 case WNil{}:
5577 {==}
5578 case WCon{True{}, w8}:
5579 match w8:
5580 case WNil{}:
5581 {==}
5582 case WCon{True{}, w3}:
5583 match w3:
5584 case WCon{False{}, w4}:
5585 match w4:
5586 case WCon{False{}, w5}:
5587 match w5:
5588 case WCon{False{}, w6}:
5589 match w6:
5590 case WCon{False{}, w7}:
5591 match w7:
5592 case WCon{False{}, w8}:
5593 match w8:
5594 case WNil{}:
5595 {==}
5596 case WCon{True{}, w8}:
5597 match w8:
5598 case WNil{}:
5599 {==}
5600 case WCon{True{}, w7}:
5601 match w7:
5602 case WCon{False{}, w8}:
5603 match w8:
5604 case WNil{}:
5605 {==}
5606 case WCon{True{}, w8}:
5607 match w8:
5608 case WNil{}:
5609 {==}
5610 case WCon{True{}, w6}:
5611 match w6:
5612 case WCon{False{}, w7}:
5613 match w7:
5614 case WCon{False{}, w8}:
5615 match w8:
5616 case WNil{}:
5617 {==}
5618 case WCon{True{}, w8}:
5619 match w8:
5620 case WNil{}:
5621 {==}
5622 case WCon{True{}, w7}:
5623 match w7:
5624 case WCon{False{}, w8}:
5625 match w8:
5626 case WNil{}:
5627 {==}
5628 case WCon{True{}, w8}:
5629 match w8:
5630 case WNil{}:
5631 {==}
5632 case WCon{True{}, w5}:
5633 match w5:
5634 case WCon{False{}, w6}:
5635 match w6:
5636 case WCon{False{}, w7}:
5637 match w7:
5638 case WCon{False{}, w8}:
5639 match w8:
5640 case WNil{}:
5641 {==}
5642 case WCon{True{}, w8}:
5643 match w8:
5644 case WNil{}:
5645 {==}
5646 case WCon{True{}, w7}:
5647 match w7:
5648 case WCon{False{}, w8}:
5649 match w8:
5650 case WNil{}:
5651 {==}
5652 case WCon{True{}, w8}:
5653 match w8:
5654 case WNil{}:
5655 {==}
5656 case WCon{True{}, w6}:
5657 match w6:
5658 case WCon{False{}, w7}:
5659 match w7:
5660 case WCon{False{}, w8}:
5661 match w8:
5662 case WNil{}:
5663 {==}
5664 case WCon{True{}, w8}:
5665 match w8:
5666 case WNil{}:
5667 {==}
5668 case WCon{True{}, w7}:
5669 match w7:
5670 case WCon{False{}, w8}:
5671 match w8:
5672 case WNil{}:
5673 {==}
5674 case WCon{True{}, w8}:
5675 match w8:
5676 case WNil{}:
5677 {==}
5678 case WCon{True{}, w4}:
5679 match w4:
5680 case WCon{False{}, w5}:
5681 match w5:
5682 case WCon{False{}, w6}:
5683 match w6:
5684 case WCon{False{}, w7}:
5685 match w7:
5686 case WCon{False{}, w8}:
5687 match w8:
5688 case WNil{}:
5689 {==}
5690 case WCon{True{}, w8}:
5691 match w8:
5692 case WNil{}:
5693 {==}
5694 case WCon{True{}, w7}:
5695 match w7:
5696 case WCon{False{}, w8}:
5697 match w8:
5698 case WNil{}:
5699 {==}
5700 case WCon{True{}, w8}:
5701 match w8:
5702 case WNil{}:
5703 {==}
5704 case WCon{True{}, w6}:
5705 match w6:
5706 case WCon{False{}, w7}:
5707 match w7:
5708 case WCon{False{}, w8}:
5709 match w8:
5710 case WNil{}:
5711 {==}
5712 case WCon{True{}, w8}:
5713 match w8:
5714 case WNil{}:
5715 {==}
5716 case WCon{True{}, w7}:
5717 match w7:
5718 case WCon{False{}, w8}:
5719 match w8:
5720 case WNil{}:
5721 {==}
5722 case WCon{True{}, w8}:
5723 match w8:
5724 case WNil{}:
5725 {==}
5726 case WCon{True{}, w5}:
5727 match w5:
5728 case WCon{False{}, w6}:
5729 match w6:
5730 case WCon{False{}, w7}:
5731 match w7:
5732 case WCon{False{}, w8}:
5733 match w8:
5734 case WNil{}:
5735 {==}
5736 case WCon{True{}, w8}:
5737 match w8:
5738 case WNil{}:
5739 {==}
5740 case WCon{True{}, w7}:
5741 match w7:
5742 case WCon{False{}, w8}:
5743 match w8:
5744 case WNil{}:
5745 {==}
5746 case WCon{True{}, w8}:
5747 match w8:
5748 case WNil{}:
5749 {==}
5750 case WCon{True{}, w6}:
5751 match w6:
5752 case WCon{False{}, w7}:
5753 match w7:
5754 case WCon{False{}, w8}:
5755 match w8:
5756 case WNil{}:
5757 {==}
5758 case WCon{True{}, w8}:
5759 match w8:
5760 case WNil{}:
5761 {==}
5762 case WCon{True{}, w7}:
5763 match w7:
5764 case WCon{False{}, w8}:
5765 match w8:
5766 case WNil{}:
5767 {==}
5768 case WCon{True{}, w8}:
5769 match w8:
5770 case WNil{}:
5771 {==}
5772 case WCon{True{}, w2}:
5773 match w2:
5774 case WCon{False{}, w3}:
5775 match w3:
5776 case WCon{False{}, w4}:
5777 match w4:
5778 case WCon{False{}, w5}:
5779 match w5:
5780 case WCon{False{}, w6}:
5781 match w6:
5782 case WCon{False{}, w7}:
5783 match w7:
5784 case WCon{False{}, w8}:
5785 match w8:
5786 case WNil{}:
5787 {==}
5788 case WCon{True{}, w8}:
5789 match w8:
5790 case WNil{}:
5791 {==}
5792 case WCon{True{}, w7}:
5793 match w7:
5794 case WCon{False{}, w8}:
5795 match w8:
5796 case WNil{}:
5797 {==}
5798 case WCon{True{}, w8}:
5799 match w8:
5800 case WNil{}:
5801 {==}
5802 case WCon{True{}, w6}:
5803 match w6:
5804 case WCon{False{}, w7}:
5805 match w7:
5806 case WCon{False{}, w8}:
5807 match w8:
5808 case WNil{}:
5809 {==}
5810 case WCon{True{}, w8}:
5811 match w8:
5812 case WNil{}:
5813 {==}
5814 case WCon{True{}, w7}:
5815 match w7:
5816 case WCon{False{}, w8}:
5817 match w8:
5818 case WNil{}:
5819 {==}
5820 case WCon{True{}, w8}:
5821 match w8:
5822 case WNil{}:
5823 {==}
5824 case WCon{True{}, w5}:
5825 match w5:
5826 case WCon{False{}, w6}:
5827 match w6:
5828 case WCon{False{}, w7}:
5829 match w7:
5830 case WCon{False{}, w8}:
5831 match w8:
5832 case WNil{}:
5833 {==}
5834 case WCon{True{}, w8}:
5835 match w8:
5836 case WNil{}:
5837 {==}
5838 case WCon{True{}, w7}:
5839 match w7:
5840 case WCon{False{}, w8}:
5841 match w8:
5842 case WNil{}:
5843 {==}
5844 case WCon{True{}, w8}:
5845 match w8:
5846 case WNil{}:
5847 {==}
5848 case WCon{True{}, w6}:
5849 match w6:
5850 case WCon{False{}, w7}:
5851 match w7:
5852 case WCon{False{}, w8}:
5853 match w8:
5854 case WNil{}:
5855 {==}
5856 case WCon{True{}, w8}:
5857 match w8:
5858 case WNil{}:
5859 {==}
5860 case WCon{True{}, w7}:
5861 match w7:
5862 case WCon{False{}, w8}:
5863 match w8:
5864 case WNil{}:
5865 {==}
5866 case WCon{True{}, w8}:
5867 match w8:
5868 case WNil{}:
5869 {==}
5870 case WCon{True{}, w4}:
5871 match w4:
5872 case WCon{False{}, w5}:
5873 match w5:
5874 case WCon{False{}, w6}:
5875 match w6:
5876 case WCon{False{}, w7}:
5877 match w7:
5878 case WCon{False{}, w8}:
5879 match w8:
5880 case WNil{}:
5881 {==}
5882 case WCon{True{}, w8}:
5883 match w8:
5884 case WNil{}:
5885 {==}
5886 case WCon{True{}, w7}:
5887 match w7:
5888 case WCon{False{}, w8}:
5889 match w8:
5890 case WNil{}:
5891 {==}
5892 case WCon{True{}, w8}:
5893 match w8:
5894 case WNil{}:
5895 {==}
5896 case WCon{True{}, w6}:
5897 match w6:
5898 case WCon{False{}, w7}:
5899 match w7:
5900 case WCon{False{}, w8}:
5901 match w8:
5902 case WNil{}:
5903 {==}
5904 case WCon{True{}, w8}:
5905 match w8:
5906 case WNil{}:
5907 {==}
5908 case WCon{True{}, w7}:
5909 match w7:
5910 case WCon{False{}, w8}:
5911 match w8:
5912 case WNil{}:
5913 {==}
5914 case WCon{True{}, w8}:
5915 match w8:
5916 case WNil{}:
5917 {==}
5918 case WCon{True{}, w5}:
5919 match w5:
5920 case WCon{False{}, w6}:
5921 match w6:
5922 case WCon{False{}, w7}:
5923 match w7:
5924 case WCon{False{}, w8}:
5925 match w8:
5926 case WNil{}:
5927 {==}
5928 case WCon{True{}, w8}:
5929 match w8:
5930 case WNil{}:
5931 {==}
5932 case WCon{True{}, w7}:
5933 match w7:
5934 case WCon{False{}, w8}:
5935 match w8:
5936 case WNil{}:
5937 {==}
5938 case WCon{True{}, w8}:
5939 match w8:
5940 case WNil{}:
5941 {==}
5942 case WCon{True{}, w6}:
5943 match w6:
5944 case WCon{False{}, w7}:
5945 match w7:
5946 case WCon{False{}, w8}:
5947 match w8:
5948 case WNil{}:
5949 {==}
5950 case WCon{True{}, w8}:
5951 match w8:
5952 case WNil{}:
5953 {==}
5954 case WCon{True{}, w7}:
5955 match w7:
5956 case WCon{False{}, w8}:
5957 match w8:
5958 case WNil{}:
5959 {==}
5960 case WCon{True{}, w8}:
5961 match w8:
5962 case WNil{}:
5963 {==}
5964 case WCon{True{}, w3}:
5965 match w3:
5966 case WCon{False{}, w4}:
5967 match w4:
5968 case WCon{False{}, w5}:
5969 match w5:
5970 case WCon{False{}, w6}:
5971 match w6:
5972 case WCon{False{}, w7}:
5973 match w7:
5974 case WCon{False{}, w8}:
5975 match w8:
5976 case WNil{}:
5977 {==}
5978 case WCon{True{}, w8}:
5979 match w8:
5980 case WNil{}:
5981 {==}
5982 case WCon{True{}, w7}:
5983 match w7:
5984 case WCon{False{}, w8}:
5985 match w8:
5986 case WNil{}:
5987 {==}
5988 case WCon{True{}, w8}:
5989 match w8:
5990 case WNil{}:
5991 {==}
5992 case WCon{True{}, w6}:
5993 match w6:
5994 case WCon{False{}, w7}:
5995 match w7:
5996 case WCon{False{}, w8}:
5997 match w8:
5998 case WNil{}:
5999 {==}
6000 case WCon{True{}, w8}:
6001 match w8:
6002 case WNil{}:
6003 {==}
6004 case WCon{True{}, w7}:
6005 match w7:
6006 case WCon{False{}, w8}:
6007 match w8:
6008 case WNil{}:
6009 {==}
6010 case WCon{True{}, w8}:
6011 match w8:
6012 case WNil{}:
6013 {==}
6014 case WCon{True{}, w5}:
6015 match w5:
6016 case WCon{False{}, w6}:
6017 match w6:
6018 case WCon{False{}, w7}:
6019 match w7:
6020 case WCon{False{}, w8}:
6021 match w8:
6022 case WNil{}:
6023 {==}
6024 case WCon{True{}, w8}:
6025 match w8:
6026 case WNil{}:
6027 {==}
6028 case WCon{True{}, w7}:
6029 match w7:
6030 case WCon{False{}, w8}:
6031 match w8:
6032 case WNil{}:
6033 {==}
6034 case WCon{True{}, w8}:
6035 match w8:
6036 case WNil{}:
6037 {==}
6038 case WCon{True{}, w6}:
6039 match w6:
6040 case WCon{False{}, w7}:
6041 match w7:
6042 case WCon{False{}, w8}:
6043 match w8:
6044 case WNil{}:
6045 {==}
6046 case WCon{True{}, w8}:
6047 match w8:
6048 case WNil{}:
6049 {==}
6050 case WCon{True{}, w7}:
6051 match w7:
6052 case WCon{False{}, w8}:
6053 match w8:
6054 case WNil{}:
6055 {==}
6056 case WCon{True{}, w8}:
6057 match w8:
6058 case WNil{}:
6059 {==}
6060 case WCon{True{}, w4}:
6061 match w4:
6062 case WCon{False{}, w5}:
6063 match w5:
6064 case WCon{False{}, w6}:
6065 match w6:
6066 case WCon{False{}, w7}:
6067 match w7:
6068 case WCon{False{}, w8}:
6069 match w8:
6070 case WNil{}:
6071 {==}
6072 case WCon{True{}, w8}:
6073 match w8:
6074 case WNil{}:
6075 {==}
6076 case WCon{True{}, w7}:
6077 match w7:
6078 case WCon{False{}, w8}:
6079 match w8:
6080 case WNil{}:
6081 {==}
6082 case WCon{True{}, w8}:
6083 match w8:
6084 case WNil{}:
6085 {==}
6086 case WCon{True{}, w6}:
6087 match w6:
6088 case WCon{False{}, w7}:
6089 match w7:
6090 case WCon{False{}, w8}:
6091 match w8:
6092 case WNil{}:
6093 {==}
6094 case WCon{True{}, w8}:
6095 match w8:
6096 case WNil{}:
6097 {==}
6098 case WCon{True{}, w7}:
6099 match w7:
6100 case WCon{False{}, w8}:
6101 match w8:
6102 case WNil{}:
6103 {==}
6104 case WCon{True{}, w8}:
6105 match w8:
6106 case WNil{}:
6107 {==}
6108 case WCon{True{}, w5}:
6109 match w5:
6110 case WCon{False{}, w6}:
6111 match w6:
6112 case WCon{False{}, w7}:
6113 match w7:
6114 case WCon{False{}, w8}:
6115 match w8:
6116 case WNil{}:
6117 {==}
6118 case WCon{True{}, w8}:
6119 match w8:
6120 case WNil{}:
6121 {==}
6122 case WCon{True{}, w7}:
6123 match w7:
6124 case WCon{False{}, w8}:
6125 match w8:
6126 case WNil{}:
6127 {==}
6128 case WCon{True{}, w8}:
6129 match w8:
6130 case WNil{}:
6131 {==}
6132 case WCon{True{}, w6}:
6133 match w6:
6134 case WCon{False{}, w7}:
6135 match w7:
6136 case WCon{False{}, w8}:
6137 match w8:
6138 case WNil{}:
6139 {==}
6140 case WCon{True{}, w8}:
6141 match w8:
6142 case WNil{}:
6143 {==}
6144 case WCon{True{}, w7}:
6145 match w7:
6146 case WCon{False{}, w8}:
6147 match w8:
6148 case WNil{}:
6149 {==}
6150 case WCon{True{}, w8}:
6151 match w8:
6152 case WNil{}:
6153 {==}