path: "vendor/opentheory/data/theories/natural-bits-def/natural-bits-def.art"
6 version nil "P" "->" typeOp 0 def "Number.Natural.natural" typeOp nil opType 1 def "bool" typeOp nil opType 2 def nil cons 3 def cons opType 4 def var 5 def "n" 1 ref var 6 def "=" const 7 def 0 ref 2 ref 0 ref 2 ref 3 ref cons opType 8 def nil cons cons opType 9 def constTerm 10 def "Number.Natural.Bits.head" "_28510" 1 ref var 11 def "Number.Natural.odd" const 4 ref constTerm 12 def 11 ref varTerm 13 def appTerm 14 def absTerm 15 def defineConst 16 def pop 4 ref constTerm 17 def 6 ref varTerm 18 def appTerm 19 def appTerm 12 remove 18 ref appTerm appTerm absTerm 20 def nil cons cons nil cons nil cons cons "A" 1 ref nil cons 21 def cons nil cons 22 def nil nil cons 23 def cons 24 def 10 ref "Data.Bool.!" const 25 def 0 ref 0 ref "A" varType 26 def 3 ref cons opType 27 def 3 ref cons opType 28 def constTerm 29 def "P" 27 ref var 30 def varTerm 31 def appTerm 32 def appTerm refl "p" 27 ref var 33 def 7 ref 0 ref 27 ref 28 ref nil cons cons opType constTerm 33 ref varTerm 34 def appTerm "x" 26 ref var 35 def "Data.Bool.T" const 2 ref constTerm 36 def absTerm 37 def appTerm absTerm 38 def 31 ref appTerm betaConv 39 def appThm nil 7 ref 0 ref 28 ref 0 ref 28 ref 3 ref cons opType 40 def nil cons cons opType constTerm 41 def 29 ref appTerm 38 remove appTerm axiom 31 ref refl 42 def appThm 43 def eqMp sym 44 def subst 45 def subst 11 remove nil "t" 2 ref var 46 def 10 ref 17 ref 13 ref appTerm appTerm 14 remove appTerm nil cons cons nil cons nil cons cons 10 ref 46 ref varTerm 47 def appTerm 48 def 36 ref appTerm 49 def assume sym nil 36 ref axiom 50 def eqMp 47 ref assume 50 ref deductAntisym deductAntisym 51 def subst 16 remove 13 ref refl appThm 15 remove 13 remove appTerm betaConv trans eqMp absThm eqMp nil 25 ref 0 ref 4 ref 3 ref cons opType constTerm 52 def 20 remove appTerm thm "Number.Natural.Bits.toVector" "num_to_bitvec" 0 ref 1 ref 0 ref 1 ref "Data.List.list" typeOp 53 def 3 ref opType 54 def nil cons 55 def cons opType 56 def nil cons 57 def cons opType 58 def var 59 def nil cons cons nil cons 59 ref "Data.Bool./\\" const 9 ref constTerm 60 def 52 ref 6 ref 7 ref 0 ref 54 ref 0 ref 54 ref 3 ref cons opType 61 def nil cons cons opType constTerm 62 def 59 ref varTerm 63 def 18 ref appTerm 64 def "Number.Natural.zero" const 1 ref constTerm 65 def appTerm appTerm "Data.List.[]" const 54 ref constTerm 66 def appTerm absTerm appTerm appTerm 52 ref 6 ref 52 ref "k" 1 ref var 67 def 62 ref 64 remove "Number.Natural.suc" const 0 ref 1 ref 21 ref cons opType 68 def constTerm 69 def 67 ref varTerm 70 def appTerm 71 def appTerm appTerm "Data.List.::" const 0 ref 2 ref 0 ref 54 ref 55 ref cons opType nil cons cons opType constTerm 72 def 19 remove appTerm 73 def 63 ref "Number.Natural.Bits.tail" "_28515" 1 ref var 74 def "Number.Natural.div" const 0 ref 1 ref 68 ref nil cons 75 def cons opType 76 def constTerm 77 def 74 ref varTerm 78 def appTerm "Number.Natural.bit0" const 68 ref constTerm "Number.Natural.bit1" const 68 ref constTerm 65 ref appTerm 79 def appTerm 80 def appTerm 81 def absTerm 82 def defineConst 83 def pop 68 ref constTerm 84 def 18 ref appTerm 85 def appTerm 70 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 86 def refl 87 def 7 ref 0 ref 58 ref 0 ref 58 ref 3 ref cons opType 88 def nil cons cons opType constTerm 89 def 63 ref appTerm 90 def "select" const 91 def 0 ref 88 ref 58 ref nil cons 92 def cons opType constTerm 93 def 86 ref appTerm appTerm assume sym appThm 86 ref 63 ref appTerm betaConv 94 def trans "A" 92 ref cons nil cons 95 def 23 ref cons 96 def nil 41 ref "Data.Bool.?" const 97 def 28 ref constTerm 98 def appTerm 99 def 33 ref 34 ref 91 ref 0 ref 27 ref 26 ref nil cons 100 def cons opType constTerm 34 ref appTerm appTerm 101 def absTerm appTerm axiom 102 def subst 87 remove appThm "p" 88 ref var 103 def 103 remove varTerm 104 def 93 remove 104 remove appTerm appTerm absTerm 86 ref appTerm betaConv trans 97 ref 0 ref 88 ref 3 ref cons opType 105 def constTerm 106 def refl "fn" 58 ref var 107 def 60 ref 7 ref 0 ref 56 ref 0 ref 56 ref 3 ref cons opType nil cons cons opType constTerm 108 def 107 remove varTerm 109 def 65 ref appTerm appTerm 6 ref 66 ref absTerm 110 def appTerm appTerm refl 52 ref refl 111 def 6 ref 108 ref 109 ref 69 remove 18 ref appTerm 112 def appTerm appTerm refl "_28609" 56 ref var 113 def 67 ref 6 ref 73 ref 113 remove varTerm 85 ref appTerm appTerm absTerm absTerm absTerm 114 def 109 remove 18 ref appTerm 115 def appTerm betaConv 18 ref refl 116 def appThm 67 ref "n'" 1 ref var 117 def 72 remove 17 ref 117 ref varTerm 118 def appTerm appTerm 119 def 115 remove 84 ref 118 remove appTerm 120 def appTerm appTerm absTerm absTerm 18 ref appTerm betaConv trans appThm absThm appThm appThm absThm appThm nil "f" 0 ref 56 ref 92 remove cons opType var 114 remove nil cons cons "e" 56 ref var 110 ref nil cons cons nil cons cons nil cons cons "A" 57 remove cons nil cons 23 ref cons "f" 0 ref 26 ref 0 ref 1 ref 100 ref cons opType 121 def nil cons 122 def cons opType 123 def var 124 def "Data.Bool.?!" const 125 def 0 ref 0 ref 121 ref 3 ref cons opType 126 def 3 ref cons opType 127 def constTerm "fn" 121 remove var 128 def 60 ref 7 ref 0 ref 26 ref 27 ref nil cons 129 def cons opType constTerm 130 def 128 remove varTerm 131 def 65 ref appTerm appTerm "e" 26 ref var 132 def varTerm 133 def appTerm appTerm 52 ref 6 ref 130 ref 131 ref 112 ref appTerm appTerm 124 remove varTerm 134 def 131 remove 18 ref appTerm appTerm 18 ref appTerm appTerm absTerm appTerm appTerm absTerm 135 def appTerm 136 def absTerm 137 def 134 ref appTerm 138 def betaConv 132 remove 25 ref 0 ref 0 ref 123 ref 3 ref cons opType 139 def 3 ref cons opType constTerm 137 ref appTerm 140 def absTerm 141 def 133 ref appTerm 142 def betaConv nil 29 ref 141 ref appTerm 143 def axiom nil "p" 2 ref var 144 def 143 remove nil cons cons "q" 2 ref var 145 def 142 remove nil cons cons nil cons cons nil cons cons 10 ref "Data.Bool.==>" const 9 ref constTerm 146 def 144 ref varTerm 147 def appTerm 148 def 145 ref varTerm 149 def appTerm 150 def appTerm 151 def refl 144 ref 145 ref 10 ref 60 ref 147 ref appTerm 152 def 149 ref appTerm 153 def appTerm 154 def 147 ref appTerm absTerm 155 def absTerm 156 def 147 ref appTerm betaConv 149 ref refl 157 def appThm 155 remove 149 ref appTerm betaConv trans appThm nil 7 ref 0 ref 9 ref 0 ref 9 ref 3 ref cons opType 158 def nil cons cons opType constTerm 159 def 146 ref appTerm 156 remove appTerm axiom 147 ref refl 160 def appThm 157 ref appThm eqMp 161 def sym 162 def 154 remove refl 145 ref 7 ref 0 ref 158 ref 0 ref 158 remove 3 ref cons opType nil cons cons opType constTerm 163 def "f" 9 ref var 164 def 164 ref varTerm 165 def 147 ref appTerm 149 ref appTerm absTerm 166 def appTerm 164 ref 165 ref 36 ref appTerm 36 ref appTerm absTerm 167 def appTerm absTerm 168 def 149 ref appTerm betaConv appThm 7 ref 0 ref 8 ref 0 ref 8 ref 3 ref cons opType 169 def nil cons cons opType constTerm 170 def 152 remove appTerm refl 144 ref 168 remove absTerm 171 def 147 ref appTerm betaConv appThm nil 159 ref 60 ref appTerm 171 ref appTerm axiom 172 def 160 remove appThm eqMp 157 ref appThm eqMp 173 def sym 164 ref 165 ref refl nil 46 ref 147 ref nil cons 174 def cons nil cons nil cons cons 51 ref subst 147 ref assume 175 def eqMp appThm nil 46 ref 149 ref nil cons 176 def cons nil cons nil cons cons 51 ref subst 149 ref assume 177 def eqMp appThm absThm eqMp 178 def nil "P" 2 ref var 179 def 174 ref cons "Q" 2 ref var 180 def 176 ref cons nil cons 181 def cons nil cons cons 10 ref refl 182 def 164 ref 165 remove 179 ref varTerm 183 def appTerm 184 def 180 ref varTerm 185 def appTerm absTerm 186 def 144 ref 145 ref 147 ref absTerm absTerm 187 def appTerm betaConv 187 ref 183 ref appTerm betaConv 185 ref refl 188 def appThm 145 ref 183 ref absTerm 185 ref appTerm betaConv trans trans appThm 167 ref 187 ref appTerm betaConv 187 ref 36 ref appTerm betaConv 36 ref refl 189 def appThm 145 ref 36 ref absTerm 36 ref appTerm betaConv trans trans appThm 10 ref 60 ref 183 ref appTerm 190 def 185 ref appTerm 191 def appTerm refl 145 ref 163 remove 164 remove 184 remove 149 ref appTerm absTerm appTerm 167 ref appTerm absTerm 185 ref appTerm betaConv appThm 170 ref 190 remove appTerm refl 171 remove 183 ref appTerm betaConv appThm 172 remove 183 ref refl 192 def appThm eqMp 188 ref appThm eqMp 191 remove assume eqMp 193 def 187 remove refl appThm eqMp sym 50 ref eqMp 194 def subst 195 def deductAntisym eqMp 161 remove 150 ref assume eqMp sym 175 ref eqMp 182 ref 166 remove 144 ref 145 ref 149 ref absTerm 196 def absTerm 197 def appTerm betaConv 197 ref 147 ref appTerm betaConv 157 remove appThm 196 ref 149 ref appTerm betaConv trans trans appThm 167 remove 197 ref appTerm betaConv 197 ref 36 ref appTerm betaConv 189 remove appThm 196 ref 36 ref appTerm betaConv trans trans 198 def appThm 173 remove 153 remove assume eqMp 197 ref refl 199 def appThm eqMp sym 50 ref eqMp 200 def proveHyp 201 def deductAntisym 202 def subst proveHyp "A" 100 ref cons 203 def nil cons 204 def 30 ref 141 remove nil cons cons 35 ref 133 remove nil cons cons nil cons cons nil cons cons nil 144 ref 32 ref nil cons 205 def cons 145 ref 31 ref 35 ref varTerm 206 def appTerm 207 def nil cons 208 def cons nil cons cons nil cons cons 209 def 162 ref subst 209 remove 200 remove 178 remove deductAntisym 210 def subst 10 ref 207 ref appTerm refl 37 remove 206 ref appTerm betaConv appThm 39 remove 43 remove 32 remove assume eqMp eqMp 206 ref refl 211 def appThm eqMp sym 50 ref eqMp eqMp nil 179 ref 205 remove cons 180 ref 208 ref cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp 212 def subst eqMp eqMp nil 144 ref 140 remove nil cons cons 145 ref 138 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 123 ref nil cons cons nil cons "P" 139 remove var 137 remove nil cons cons "x" 123 remove var 134 remove nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 136 remove nil cons cons 145 ref 97 ref 127 remove constTerm 135 ref appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 122 remove cons nil cons "P" 126 remove var 135 remove nil cons cons nil cons nil cons cons nil 144 ref 125 remove 28 ref constTerm 213 def 31 ref appTerm 214 def nil cons 215 def cons 216 def 145 ref 98 ref 31 ref appTerm 217 def nil cons 218 def cons nil cons cons nil cons cons 219 def 162 ref subst 219 remove 210 ref subst nil 216 remove 145 ref 60 ref 217 ref appTerm 29 ref 35 ref 29 ref "y" 26 ref var 220 def 146 ref 60 ref 207 ref appTerm 31 ref 220 ref varTerm 221 def appTerm appTerm appTerm 130 ref 206 ref appTerm 222 def 221 ref appTerm 223 def appTerm absTerm appTerm absTerm appTerm 224 def appTerm 225 def nil cons cons nil cons cons nil cons cons 226 def 202 ref subst 10 ref 214 ref appTerm 227 def refl 33 ref 60 ref 98 ref 34 ref appTerm 228 def appTerm 29 ref 35 ref 29 ref 220 remove 146 ref 60 ref 34 ref 206 ref appTerm 229 def appTerm 34 ref 221 remove appTerm appTerm appTerm 223 remove appTerm absTerm appTerm absTerm appTerm appTerm absTerm 230 def 31 ref appTerm betaConv appThm nil 41 remove 213 remove appTerm 230 remove appTerm axiom 42 ref appThm eqMp nil 144 ref 227 remove 225 ref appTerm nil cons cons 145 ref 146 ref 214 remove appTerm 225 remove appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 226 remove nil 144 ref 10 ref 147 ref appTerm 231 def 149 ref appTerm 232 def nil cons 233 def cons 234 def 145 ref 150 ref nil cons 235 def cons nil cons 236 def cons nil cons cons 237 def 162 ref subst 237 remove 210 ref subst 162 ref 210 ref 232 remove assume 238 def 175 remove eqMp eqMp 195 ref deductAntisym eqMp 239 def eqMp nil 179 ref 233 remove cons 240 def 180 ref 235 ref cons nil cons 241 def cons nil cons cons 194 ref subst deductAntisym eqMp 242 def subst eqMp eqMp nil 179 ref 218 ref cons 243 def 180 ref 224 remove nil cons cons nil cons cons nil cons cons 194 ref subst proveHyp eqMp nil 179 ref 215 remove cons 180 ref 218 ref cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp subst eqMp subst subst eqMp nil 144 ref 106 ref "_28608" 58 ref var 244 def 60 ref 108 ref 244 ref varTerm 245 def 65 ref appTerm 246 def appTerm 110 ref appTerm 247 def appTerm 248 def 52 ref 67 ref 108 ref 245 ref 71 ref appTerm 249 def appTerm 6 ref 73 ref 245 ref 70 ref appTerm 85 ref appTerm appTerm 250 def absTerm 251 def appTerm absTerm 252 def appTerm 253 def appTerm 254 def absTerm 255 def appTerm 256 def nil cons cons 145 ref 106 ref 244 ref 60 ref 52 ref 6 ref 62 ref 246 remove 18 ref appTerm appTerm 257 def 66 ref appTerm 258 def absTerm 259 def appTerm 260 def appTerm 52 ref 6 ref 52 ref 67 ref 62 ref 249 remove 18 ref appTerm appTerm 261 def 250 remove appTerm 262 def absTerm 263 def appTerm 264 def absTerm 265 def appTerm 266 def appTerm 267 def absTerm 268 def appTerm 269 def nil cons 270 def cons nil cons 271 def cons nil cons cons 202 ref subst nil "P" 88 remove var 272 def 244 ref 146 ref 255 ref 245 ref appTerm 273 def appTerm 269 ref appTerm 274 def absTerm nil cons cons nil cons nil cons cons 96 remove 44 ref subst 275 def subst 244 ref nil 46 ref 274 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 273 remove nil cons 276 def cons 271 ref cons nil cons cons 277 def 162 ref subst 277 remove 210 ref subst 244 ref 248 remove 52 ref 6 ref 108 remove 245 ref 112 remove appTerm appTerm 117 remove 119 remove 245 ref 18 ref appTerm 120 remove appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 245 ref appTerm 278 def betaConv 278 remove assume eqMp nil 144 ref 254 remove nil cons 279 def cons 271 remove cons nil cons cons 280 def 202 ref subst proveHyp 280 ref 162 ref subst 280 remove 210 ref subst 268 ref 245 ref appTerm 281 def betaConv 282 def sym nil 179 ref 247 ref nil cons cons 180 ref 253 remove nil cons 283 def cons nil cons cons nil cons cons 284 def 194 ref subst nil 5 ref 259 remove nil cons cons nil cons nil cons cons 45 ref subst 6 ref nil 46 ref 258 remove nil cons cons nil cons nil cons cons 51 ref subst 257 remove refl 110 remove 18 ref appTerm betaConv appThm 247 remove assume 116 ref appThm eqMp eqMp absThm eqMp proveHyp nil 144 ref 260 remove nil cons cons 145 ref 266 remove nil cons cons nil cons cons nil cons cons 210 ref subst proveHyp 284 remove 182 ref 186 remove 197 ref appTerm betaConv 197 remove 183 ref appTerm betaConv 188 ref appThm 196 remove 185 ref appTerm betaConv trans trans appThm 198 remove appThm 193 remove 199 remove appThm eqMp sym 50 ref eqMp 285 def subst nil 5 ref 265 remove nil cons cons nil cons nil cons cons 45 ref subst 6 ref nil 46 ref 264 remove nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 263 remove nil cons cons nil cons nil cons cons 45 ref subst 67 ref nil 46 ref 262 remove nil cons cons nil cons nil cons cons 51 ref subst 261 remove refl 251 remove 18 ref appTerm betaConv appThm 252 ref 70 ref appTerm 286 def betaConv nil 144 ref 283 remove cons 145 ref 286 remove nil cons cons nil cons cons nil cons cons 202 ref subst 22 ref 5 ref 252 remove nil cons cons "x" 1 ref var 287 def 70 ref nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp 116 ref appThm eqMp eqMp absThm eqMp eqMp absThm eqMp proveHyp eqMp eqMp 95 ref 272 ref 268 ref nil cons cons 288 def "x" 58 ref var 289 def 245 ref nil cons cons nil cons cons nil cons cons 10 ref 217 ref appTerm 290 def refl 33 ref 25 ref 169 remove constTerm 291 def 145 ref 146 ref 29 ref 35 ref 146 ref 229 ref appTerm 292 def 149 ref appTerm absTerm appTerm appTerm 149 ref appTerm absTerm appTerm absTerm 293 def 31 remove appTerm betaConv appThm nil 99 remove 293 remove appTerm axiom 42 remove appThm eqMp 294 def sym nil "P" 8 ref var 295 def 180 ref 146 ref 29 ref 35 ref 146 ref 207 ref appTerm 296 def 185 ref appTerm 297 def absTerm 298 def appTerm 299 def appTerm 300 def 185 ref appTerm 301 def absTerm nil cons cons nil cons nil cons cons "A" 3 ref cons nil cons 302 def 23 ref cons 44 ref subst 303 def subst 180 ref nil 46 ref 301 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 299 ref nil cons 304 def cons 305 def 145 ref 185 ref nil cons 306 def cons nil cons 307 def cons nil cons cons 308 def 162 ref subst 308 ref 210 ref subst nil 144 ref 208 ref cons 307 ref cons nil cons cons 309 def 202 ref subst 310 def 298 ref 206 ref appTerm 311 def betaConv nil 305 ref 145 ref 311 remove nil cons cons nil cons cons nil cons cons 202 ref subst 204 ref 30 ref 298 remove nil cons cons 312 def 35 ref 206 ref nil cons cons nil cons 313 def cons nil cons cons 212 ref subst eqMp eqMp 314 def eqMp eqMp nil 179 ref 304 ref cons 315 def 180 ref 306 ref cons nil cons 316 def cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 317 def subst proveHyp eqMp nil 179 ref 279 remove cons 180 ref 270 ref cons nil cons 318 def cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp nil 179 ref 276 remove cons 318 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp nil 144 ref 25 ref 105 remove constTerm 319 def 289 ref 146 ref 255 ref 289 ref varTerm 320 def appTerm appTerm 269 ref appTerm absTerm appTerm nil cons cons 145 ref 146 ref 256 remove appTerm 269 ref appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 95 ref 272 ref 255 remove nil cons cons 318 remove cons nil cons cons nil 305 ref 145 ref 146 ref 217 remove appTerm 321 def 185 ref appTerm nil cons 322 def cons nil cons cons nil cons cons 323 def 162 ref subst 323 remove 210 ref subst nil 144 ref 218 remove cons 324 def 307 ref cons nil cons cons 325 def 162 ref subst 325 remove 210 ref subst 308 remove 202 ref subst 145 ref 146 ref 29 ref 35 ref 296 remove 149 ref appTerm absTerm appTerm appTerm 149 ref appTerm absTerm 326 def 185 ref appTerm 327 def betaConv nil 324 remove 145 ref 291 ref 326 ref appTerm 328 def nil cons 329 def cons nil cons cons nil cons cons 330 def 202 ref subst 294 remove nil 144 ref 290 remove 328 ref appTerm nil cons cons 145 ref 321 remove 328 remove appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 330 remove 242 ref subst eqMp eqMp nil 144 ref 329 remove cons 145 ref 327 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 302 ref 295 ref 326 remove nil cons cons "x" 2 ref var 331 def 306 remove cons nil cons cons nil cons cons 212 ref subst eqMp eqMp eqMp eqMp nil 243 remove 316 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp nil 315 ref 180 ref 322 remove cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp 332 def subst eqMp eqMp proveHyp nil 144 ref 270 remove cons 145 ref 106 remove 86 ref appTerm 333 def nil cons 334 def cons nil cons 335 def cons nil cons cons 202 ref subst nil 272 ref 244 ref 146 ref 281 ref appTerm 333 ref appTerm 336 def absTerm nil cons cons nil cons nil cons cons 275 remove subst 244 remove nil 46 ref 336 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 281 ref nil cons 337 def cons 335 ref cons nil cons cons 338 def 162 ref subst 338 remove 210 ref subst 282 remove 281 remove assume eqMp nil 144 ref 267 ref nil cons 339 def cons 335 ref cons nil cons cons 340 def 202 ref subst proveHyp 340 ref 162 ref subst 340 remove 210 ref subst "_28606" 1 ref var 341 def "_28607" 1 ref var 342 def 245 remove 342 ref varTerm appTerm 343 def 341 remove varTerm appTerm absTerm absTerm 344 def refl nil 144 ref 89 remove 344 ref appTerm 344 ref appTerm nil cons cons 335 ref cons nil cons cons 202 ref subst proveHyp nil 59 remove 344 ref nil cons cons nil cons nil cons cons nil 144 ref 90 remove 344 ref appTerm 345 def nil cons 346 def cons 335 remove cons nil cons cons 347 def 162 ref subst 347 remove 210 ref subst 94 remove sym 60 ref refl 111 ref 6 ref 62 ref refl 348 def 345 remove assume 349 def 116 ref appThm 344 ref 18 ref appTerm betaConv trans 350 def nil 6 ref 65 ref nil cons cons nil cons nil cons cons 116 remove subst appThm 342 ref 343 ref 18 ref appTerm absTerm 351 def 65 ref appTerm betaConv trans appThm 66 ref refl appThm absThm appThm appThm 111 ref 6 ref 111 ref 67 ref 348 remove 350 remove 71 ref refl appThm 351 remove 71 ref appTerm betaConv trans appThm 73 ref refl 349 remove 85 ref refl appThm 344 remove 85 ref appTerm betaConv trans 70 ref refl appThm 342 remove 343 remove 85 ref appTerm absTerm 70 ref appTerm betaConv trans appThm appThm absThm appThm absThm appThm appThm sym 267 remove assume eqMp eqMp 95 ref 272 remove 86 remove nil cons cons 289 ref 63 remove nil cons cons nil cons cons nil cons cons 317 ref subst proveHyp eqMp nil 179 ref 346 remove cons 180 ref 334 remove cons nil cons 352 def cons nil cons cons 194 ref subst deductAntisym eqMp subst eqMp eqMp nil 179 ref 339 remove cons 352 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp nil 179 ref 337 remove cons 352 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp nil 144 ref 319 remove 289 remove 146 ref 268 remove 320 remove appTerm appTerm 333 ref appTerm absTerm appTerm nil cons cons 145 ref 146 ref 269 remove appTerm 333 remove appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 95 remove 288 remove 352 remove cons nil cons cons 332 ref subst eqMp eqMp proveHyp eqMp eqMp defineConstList 353 def pop 354 def pop 353 ref nil 179 ref 52 ref 6 ref 62 ref 354 remove hdTl pop 58 remove constTerm 355 def 18 ref appTerm 356 def 65 ref appTerm appTerm 66 remove appTerm absTerm appTerm 357 def nil cons cons 180 ref 52 ref 6 ref 52 ref 67 ref 62 ref 356 ref 71 remove appTerm appTerm 73 remove 355 ref 85 ref appTerm 70 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm 358 def nil cons cons nil cons cons nil cons cons 359 def 194 ref subst proveHyp nil 357 remove thm nil "P" 61 ref var 360 def "l" 54 ref var 361 def 7 ref 0 ref 1 ref 4 ref nil cons cons opType 362 def constTerm 363 def "Number.Natural.Bits.fromList" "_28601" 54 ref var 364 def "Number.Natural.Bits.append" "_28589" 54 ref var 365 def "_28590" 1 ref var 366 def "Data.List.foldr" const 0 ref 0 ref 2 ref 75 ref cons opType 367 def 0 ref 1 ref 0 ref 54 ref 21 ref cons opType 368 def nil cons cons opType nil cons cons opType constTerm "Number.Natural.Bits.cons" "_28498" 2 ref var 369 def "_28499" 1 ref var 370 def "Number.Natural.+" const 76 ref constTerm 371 def "Number.Natural.fromBool" "_28493" 2 ref var 372 def "Data.Bool.cond" const 373 def 0 ref 2 ref 76 ref nil cons cons opType constTerm 374 def 372 ref varTerm 375 def appTerm 79 ref appTerm 65 ref appTerm 376 def absTerm 377 def defineConst 378 def pop 0 ref 2 ref 21 ref cons opType constTerm 379 def 369 ref varTerm 380 def appTerm appTerm "Number.Natural.*" const 76 ref constTerm 381 def 80 ref appTerm 382 def 370 ref varTerm 383 def appTerm appTerm 384 def absTerm 385 def absTerm 386 def defineConst 387 def pop 367 remove constTerm 388 def appTerm 389 def 366 ref varTerm 390 def appTerm 365 ref varTerm 391 def appTerm 392 def absTerm 393 def absTerm 394 def defineConst 395 def pop 0 ref 54 ref 75 remove cons opType constTerm 396 def 364 ref varTerm 397 def appTerm 65 ref appTerm 398 def absTerm 399 def defineConst 400 def pop 368 remove constTerm 401 def 361 ref varTerm 402 def appTerm 403 def appTerm 396 ref 402 ref appTerm 404 def 65 ref appTerm appTerm absTerm 405 def nil cons cons nil cons nil cons cons "A" 55 ref cons nil cons 23 ref cons 44 ref subst 406 def subst 364 remove nil 46 ref 363 ref 401 ref 397 ref appTerm appTerm 398 remove appTerm nil cons cons nil cons nil cons cons 51 ref subst 400 remove 397 ref refl appThm 399 remove 397 remove appTerm betaConv trans eqMp absThm eqMp nil 25 ref 0 ref 61 ref 3 ref cons opType constTerm 407 def 405 remove appTerm thm nil 5 ref 6 ref 62 ref "Number.Natural.Bits.toList" "_28612" 1 ref var 408 def 355 remove 408 ref varTerm 409 def appTerm "Number.Natural.Bits.width" "_28488" 1 ref var 410 def 374 ref 363 ref 410 ref varTerm 411 def appTerm 65 ref appTerm appTerm 65 ref appTerm 371 ref "Number.Natural.log" const 76 ref constTerm 80 ref appTerm 412 def 411 ref appTerm appTerm 79 ref appTerm appTerm 413 def absTerm 414 def defineConst 415 def pop 68 remove constTerm 416 def 409 ref appTerm appTerm 417 def absTerm 418 def defineConst 419 def pop 56 remove constTerm 420 def 18 ref appTerm appTerm 356 remove 416 ref 18 ref appTerm 421 def appTerm appTerm absTerm 422 def nil cons cons nil cons nil cons cons 45 ref subst 408 remove nil 46 ref 62 remove 420 remove 409 ref appTerm appTerm 417 remove appTerm nil cons cons nil cons nil cons cons 51 ref subst 419 remove 409 ref refl appThm 418 remove 409 remove appTerm betaConv trans eqMp absThm eqMp nil 52 ref 422 remove appTerm thm nil 295 ref "b" 2 ref var 423 def 363 ref 379 ref 423 remove varTerm 424 def appTerm appTerm 374 ref 424 remove appTerm 79 ref appTerm 65 ref appTerm appTerm absTerm 425 def nil cons cons nil cons nil cons cons 303 ref subst 372 remove nil 46 ref 363 ref 379 ref 375 ref appTerm appTerm 376 remove appTerm nil cons cons nil cons nil cons cons 51 ref subst 378 remove 375 ref refl appThm 377 remove 375 remove appTerm betaConv trans eqMp absThm eqMp nil 291 ref 425 remove appTerm thm nil 5 ref 6 ref 363 ref 85 remove appTerm 77 ref 18 ref appTerm 426 def 80 ref appTerm appTerm absTerm 427 def nil cons cons nil cons nil cons cons 45 ref subst 74 remove nil 46 ref 363 ref 84 remove 78 ref appTerm appTerm 81 remove appTerm nil cons cons nil cons nil cons cons 51 ref subst 83 remove 78 ref refl appThm 82 remove 78 remove appTerm betaConv trans eqMp absThm eqMp nil 52 ref 427 remove appTerm thm nil 360 ref 361 ref 10 ref "Number.Natural.Bits.normalList" "_28617" 54 remove var 428 def "Data.Bool.\\/" const 9 ref constTerm 429 def "Data.List.null" const 61 ref constTerm 430 def 428 ref varTerm 431 def appTerm appTerm "Data.List.last" const 61 ref constTerm 432 def 431 ref appTerm appTerm 433 def absTerm 434 def defineConst 435 def pop 61 remove constTerm 436 def 402 ref appTerm appTerm 429 ref 430 remove 402 ref appTerm appTerm 432 remove 402 ref appTerm appTerm appTerm absTerm 437 def nil cons cons nil cons nil cons cons 406 ref subst 428 remove nil 46 ref 10 ref 436 remove 431 ref appTerm appTerm 433 remove appTerm nil cons cons nil cons nil cons cons 51 ref subst 435 remove 431 ref refl appThm 434 remove 431 remove appTerm betaConv trans eqMp absThm eqMp nil 407 ref 437 remove appTerm thm nil 5 ref 6 ref 52 ref "i" 1 ref var 438 def 10 ref "Number.Natural.Bits.bit" "_28544" 1 ref var 439 def "_28545" 1 ref var 440 def 17 ref "Number.Natural.Bits.shiftRight" "_28532" 1 ref var 441 def "_28533" 1 ref var 442 def 77 remove 441 ref varTerm 443 def appTerm "Number.Natural.^" const 76 ref constTerm 80 remove appTerm 444 def 442 ref varTerm 445 def appTerm appTerm 446 def absTerm 447 def absTerm 448 def defineConst 449 def pop 76 ref constTerm 450 def 439 ref varTerm 451 def appTerm 440 ref varTerm 452 def appTerm appTerm 453 def absTerm 454 def absTerm 455 def defineConst 456 def pop 362 ref constTerm 457 def 18 ref appTerm 438 ref varTerm 458 def appTerm 459 def appTerm 17 remove 450 ref 18 ref appTerm 460 def 458 ref appTerm appTerm appTerm absTerm appTerm absTerm 461 def nil cons cons nil cons nil cons cons 45 ref subst 439 remove nil 46 ref 52 ref 440 ref 10 ref 457 ref 451 ref appTerm 452 ref appTerm appTerm 453 remove appTerm 462 def absTerm 463 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 463 remove nil cons cons nil cons nil cons cons 45 ref subst 440 remove nil 46 ref 462 remove nil cons cons nil cons nil cons cons 51 ref subst 456 remove 451 ref refl appThm 455 remove 451 remove appTerm betaConv trans 452 ref refl appThm 454 remove 452 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 52 ref 461 remove appTerm thm nil 360 remove 361 ref 52 ref 6 ref 363 ref 404 remove 18 ref appTerm appTerm 389 remove 18 ref appTerm 402 remove appTerm appTerm absTerm appTerm absTerm 464 def nil cons cons nil cons nil cons cons 406 remove subst 365 remove nil 46 ref 52 ref 366 ref 363 ref 396 remove 391 ref appTerm 390 ref appTerm appTerm 392 remove appTerm 465 def absTerm 466 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 466 remove nil cons cons nil cons nil cons cons 45 ref subst 366 remove nil 46 ref 465 remove nil cons cons nil cons nil cons cons 51 ref subst 395 remove 391 ref refl appThm 394 remove 391 remove appTerm betaConv trans 390 ref refl appThm 393 remove 390 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 407 remove 464 remove appTerm thm nil 5 ref 6 ref 52 ref 67 ref 363 ref "Number.Natural.Bits.bound" "_28556" 1 ref var 467 def "_28557" 1 ref var 468 def "Number.Natural.mod" const 76 ref constTerm 469 def 467 ref varTerm 470 def appTerm 444 ref 468 ref varTerm 471 def appTerm appTerm 472 def absTerm 473 def absTerm 474 def defineConst 475 def pop 76 ref constTerm 476 def 18 ref appTerm 70 ref appTerm appTerm 469 remove 18 ref appTerm 444 ref 70 ref appTerm 477 def appTerm appTerm absTerm appTerm absTerm 478 def nil cons cons nil cons nil cons cons 45 ref subst 467 remove nil 46 ref 52 ref 468 ref 363 ref 476 remove 470 ref appTerm 471 ref appTerm appTerm 472 remove appTerm 479 def absTerm 480 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 480 remove nil cons cons nil cons nil cons cons 45 ref subst 468 remove nil 46 ref 479 remove nil cons cons nil cons nil cons cons 51 ref subst 475 remove 470 ref refl appThm 474 remove 470 remove appTerm betaConv trans 471 ref refl appThm 473 remove 471 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 52 ref 478 remove appTerm thm nil 5 ref 6 ref 52 ref 67 ref 363 ref "Number.Natural.Bits.shiftLeft" "_28520" 1 ref var 481 def "_28521" 1 ref var 482 def 381 ref 444 remove 482 ref varTerm 483 def appTerm appTerm 481 ref varTerm 484 def appTerm 485 def absTerm 486 def absTerm 487 def defineConst 488 def pop 76 ref constTerm 489 def 18 ref appTerm 70 ref appTerm appTerm 381 remove 477 ref appTerm 18 ref appTerm appTerm absTerm appTerm absTerm 490 def nil cons cons nil cons nil cons cons 45 ref subst 481 remove nil 46 ref 52 ref 482 ref 363 ref 489 remove 484 ref appTerm 483 ref appTerm appTerm 485 remove appTerm 491 def absTerm 492 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 492 remove nil cons cons nil cons nil cons cons 45 ref subst 482 remove nil 46 ref 491 remove nil cons cons nil cons nil cons cons 51 ref subst 488 remove 484 ref refl appThm 487 remove 484 remove appTerm betaConv trans 483 ref refl appThm 486 remove 483 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 52 ref 490 remove appTerm thm nil 5 ref 6 ref 52 ref 67 remove 363 ref 460 remove 70 remove appTerm appTerm 426 remove 477 remove appTerm appTerm absTerm appTerm absTerm 493 def nil cons cons nil cons nil cons cons 45 ref subst 441 remove nil 46 ref 52 ref 442 ref 363 ref 450 remove 443 ref appTerm 445 ref appTerm appTerm 446 remove appTerm 494 def absTerm 495 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 495 remove nil cons cons nil cons nil cons cons 45 ref subst 442 remove nil 46 ref 494 remove nil cons cons nil cons nil cons cons 51 ref subst 449 remove 443 ref refl appThm 448 remove 443 remove appTerm betaConv trans 445 ref refl appThm 447 remove 445 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 52 ref 493 remove appTerm thm nil 295 ref "h" 2 ref var 496 def 52 ref "t" 1 ref var 497 def 363 ref 388 ref 496 remove varTerm 498 def appTerm 497 remove varTerm 499 def appTerm appTerm 371 ref 379 remove 498 remove appTerm appTerm 382 remove 499 remove appTerm appTerm appTerm absTerm appTerm absTerm 500 def nil cons cons nil cons nil cons cons 303 ref subst 369 remove nil 46 ref 52 ref 370 ref 363 ref 388 remove 380 ref appTerm 383 ref appTerm appTerm 384 remove appTerm 501 def absTerm 502 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 502 remove nil cons cons nil cons nil cons cons 45 ref subst 370 remove nil 46 ref 501 remove nil cons cons nil cons nil cons cons 51 ref subst 387 remove 380 ref refl appThm 386 remove 380 remove appTerm betaConv trans 383 ref refl appThm 385 remove 383 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 291 ref 500 remove appTerm thm 353 remove 359 remove 285 ref subst proveHyp nil 358 remove thm nil 5 ref 6 ref 25 ref 0 ref 0 ref "Probability.Random.random" typeOp nil opType 503 def 3 ref cons opType 504 def 3 ref cons opType 505 def constTerm 506 def "r" 503 ref var 507 def 363 ref "Number.Natural.Uniform.random" "_28700" 1 ref var 508 def "_28701" 503 ref var 509 def "w" 1 ref var 510 def "Number.Natural.Uniform.random.loop" "f" 0 ref 1 ref 0 ref 1 ref 0 ref 503 ref 21 ref cons opType 511 def nil cons 512 def cons opType 513 def nil cons 514 def cons opType 515 def var 516 def nil cons cons nil cons 516 ref 52 ref 6 ref 52 ref 510 ref 506 ref 507 ref 363 ref 516 ref varTerm 517 def 18 ref appTerm 518 def 510 ref varTerm 519 def appTerm 520 def 507 ref varTerm 521 def appTerm appTerm 91 ref 0 ref 0 ref 0 ref "Data.Pair.*" typeOp 522 def 503 ref 503 ref nil cons 523 def cons 524 def opType 525 def 21 ref cons opType 526 def 3 ref cons opType 527 def 526 ref nil cons 528 def cons opType constTerm 529 def "f" 526 ref var 530 def 506 ref "r1" 503 ref var 531 def 506 ref "r2" 503 ref var 532 def 363 ref 530 ref varTerm "Data.Pair.," const 533 def 0 ref 503 ref 0 ref 503 ref 525 ref nil cons 534 def cons opType 535 def nil cons cons opType constTerm 536 def 531 ref varTerm 537 def appTerm 538 def 532 ref varTerm 539 def appTerm 540 def appTerm appTerm 541 def 361 ref "m" 1 ref var 542 def 374 ref "Number.Natural.<" const 362 ref constTerm 543 def 542 ref varTerm 544 def appTerm 18 ref appTerm 545 def appTerm 544 ref appTerm 546 def 520 remove 539 ref appTerm appTerm absTerm 403 ref appTerm absTerm "Probability.Random.bits" const 0 ref 1 ref 0 ref 503 ref 55 ref cons opType nil cons cons opType constTerm 519 ref appTerm 547 def 537 ref appTerm 548 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm "Probability.Random.split" const 535 remove constTerm 521 ref appTerm 549 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 550 def refl 551 def 7 ref 0 ref 515 ref 0 ref 515 ref 3 ref cons opType 552 def nil cons cons opType constTerm 517 ref appTerm 91 ref 0 ref 552 ref 515 ref nil cons 553 def cons opType constTerm 554 def 550 ref appTerm appTerm assume sym appThm 550 ref 517 remove appTerm betaConv trans "A" 553 remove cons nil cons 23 ref cons 102 remove subst 551 remove appThm "p" 552 ref var 555 def 555 remove varTerm 556 def 554 remove 556 remove appTerm appTerm absTerm 550 remove appTerm betaConv trans 182 ref 111 ref 6 ref 97 ref 0 ref 0 ref 513 ref 3 ref cons opType 557 def 3 ref cons opType constTerm refl 558 def "f" 513 ref var 559 def 6 ref 559 ref 52 ref 510 ref 506 ref 507 ref 363 ref 559 ref varTerm 560 def 519 ref appTerm 561 def 521 ref appTerm appTerm 529 ref 530 ref 506 ref 531 ref 506 ref 532 ref 541 ref 361 ref 542 ref 546 ref 561 ref 539 ref appTerm appTerm absTerm 403 ref appTerm absTerm 548 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 549 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm 562 def absTerm 563 def 18 ref appTerm betaConv 564 def 560 ref refl appThm 562 ref 560 remove appTerm betaConv trans absThm appThm absThm appThm appThm 97 ref 0 ref 552 remove 3 ref cons opType constTerm refl 516 remove 111 ref 6 ref 564 remove 518 ref refl appThm 562 remove 518 remove appTerm betaConv trans absThm appThm absThm appThm appThm nil "r" 0 ref 1 ref 557 remove nil cons cons opType var 563 remove nil cons cons nil cons nil cons cons "B" 514 remove cons 22 ref cons 23 ref cons "r" 0 ref 26 ref 0 ref "B" varType 565 def 3 ref cons opType 566 def nil cons 567 def cons opType 568 def var 569 def 10 ref 29 ref 35 ref 97 ref 0 ref 566 ref 3 ref cons opType 570 def constTerm 571 def "y" 565 ref var 572 def 569 remove varTerm 573 def 206 ref appTerm 574 def 572 remove varTerm appTerm absTerm appTerm absTerm appTerm appTerm 97 ref 0 ref 0 ref 0 ref 26 ref 565 ref nil cons 575 def cons 576 def opType 577 def 3 ref cons opType 578 def 3 ref cons opType 579 def constTerm 580 def "f" 577 ref var 581 def 29 ref 35 ref 574 remove 581 ref varTerm 582 def 206 ref appTerm 583 def appTerm absTerm appTerm absTerm appTerm appTerm absTerm 584 def 573 ref appTerm 585 def betaConv nil 25 ref 0 ref 0 ref 568 ref 3 ref cons opType 586 def 3 ref cons opType constTerm 584 ref appTerm 587 def axiom nil 144 ref 587 remove nil cons cons 145 ref 585 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 568 ref nil cons cons nil cons "P" 586 remove var 584 remove nil cons cons "x" 568 remove var 573 remove nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp 588 def subst subst eqMp 111 ref 6 ref 182 ref 111 ref 510 ref 97 ref 0 ref 0 ref 511 ref 3 ref cons opType 589 def 3 ref cons opType 590 def constTerm 591 def refl "loop" 511 ref var 592 def 510 ref 592 ref 506 ref 507 ref 363 ref 592 ref varTerm 593 def 521 ref appTerm appTerm 529 ref 530 ref 506 ref 531 ref 506 ref 532 ref 541 ref 361 ref 542 ref 546 ref 593 ref 539 ref appTerm 594 def appTerm absTerm 595 def 403 ref appTerm absTerm 548 ref appTerm 596 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 549 ref appTerm 597 def appTerm 598 def absTerm 599 def appTerm absTerm 600 def absTerm 601 def 519 ref appTerm betaConv 602 def 593 ref refl 603 def appThm 600 ref 593 ref appTerm betaConv 604 def trans absThm appThm absThm appThm appThm 558 remove 559 remove 111 remove 510 ref 602 remove 561 ref refl appThm 600 ref 561 remove appTerm betaConv trans absThm appThm absThm appThm appThm nil "r" 0 ref 1 ref 589 ref nil cons 605 def cons opType var 601 remove nil cons cons nil cons nil cons cons "B" 512 ref cons 22 remove cons 23 ref cons 588 remove subst subst eqMp absThm appThm nil 5 ref 6 ref 52 ref 510 ref 591 ref 600 ref appTerm 606 def absTerm 607 def appTerm 608 def absTerm nil cons cons nil cons nil cons cons 45 ref subst 6 ref nil 46 ref 608 remove nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 607 remove nil cons cons nil cons nil cons cons 45 ref subst 510 ref nil 46 ref 606 ref nil cons 609 def cons nil cons nil cons cons 51 ref subst "h" 511 ref var 610 def 591 ref "f" 511 ref var 611 def 506 ref "x" 503 ref var 612 def 363 ref 611 ref varTerm 613 def 612 ref varTerm 614 def appTerm appTerm 615 def 374 ref 507 ref 91 ref 0 ref 0 ref 0 ref 525 ref 3 ref cons opType 616 def 3 ref cons opType 617 def 616 ref nil cons 618 def cons opType constTerm 619 def "f" 616 ref var 620 def 506 ref 531 ref 506 ref 532 ref 10 ref 620 ref varTerm 540 ref appTerm appTerm 621 def 361 ref 542 ref "Data.Bool.~" const 8 remove constTerm 622 def 545 ref appTerm absTerm 623 def 403 ref appTerm absTerm 548 ref appTerm 624 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 549 ref appTerm absTerm 625 def 614 ref appTerm appTerm 626 def 613 ref 507 ref 91 ref 0 ref 0 ref 0 ref 525 ref 523 ref cons opType 627 def 3 ref cons opType 627 ref nil cons cons opType constTerm 628 def "f" 627 ref var 629 def 506 ref 531 ref 506 ref 532 ref 7 ref 0 ref 503 ref 504 ref nil cons 630 def cons opType constTerm 631 def 629 ref varTerm 540 ref appTerm appTerm 632 def 361 ref 542 ref 539 ref absTerm 633 def 403 ref appTerm absTerm 548 ref appTerm 634 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 549 ref appTerm absTerm 635 def 614 ref appTerm 636 def appTerm appTerm 637 def 610 ref varTerm 614 ref appTerm 638 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm 639 def 507 ref 529 ref 530 ref 506 ref 531 ref 506 ref 532 ref 541 ref 361 ref 542 ref 544 ref absTerm 403 ref appTerm absTerm 548 ref appTerm 640 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 549 ref appTerm absTerm 641 def appTerm 642 def betaConv "g" 0 ref 524 remove opType 643 def var 644 def 25 ref 590 remove constTerm 645 def 610 ref 591 ref 611 ref 506 ref 612 ref 615 ref 626 ref 613 remove 644 ref varTerm 614 ref appTerm appTerm 646 def appTerm 638 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 647 def 635 ref appTerm 648 def betaConv "p" 504 ref var 649 def 25 ref 0 ref 0 ref 643 ref 3 ref cons opType 650 def 3 ref cons opType constTerm 651 def 644 remove 645 ref 610 remove 591 ref 611 ref 506 ref 612 ref 615 ref 374 ref 649 remove varTerm 614 ref appTerm appTerm 646 remove appTerm 638 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 652 def 625 ref appTerm 653 def betaConv "A" 523 ref cons 654 def "B" 21 ref cons nil cons cons 23 ref cons nil 25 ref 40 remove constTerm 655 def 33 ref 25 ref 0 ref 0 ref 0 ref 26 ref 100 ref cons opType 656 def 3 ref cons opType 3 ref cons opType constTerm "g" 656 ref var 657 def 25 ref 579 remove constTerm 658 def "h" 577 ref var 659 def 580 remove 581 remove 29 ref 35 ref 7 ref 0 ref 565 ref 567 remove cons opType constTerm 660 def 583 remove appTerm 373 ref 0 ref 2 ref 0 ref 565 ref 0 ref 565 ref 575 ref cons opType nil cons 661 def cons opType nil cons cons opType constTerm 229 ref appTerm 582 remove 657 remove varTerm 206 ref appTerm appTerm appTerm 659 remove varTerm 206 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm axiom subst nil 144 ref 25 ref 0 ref 505 ref 3 ref cons opType constTerm 652 ref appTerm nil cons cons 145 ref 653 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 630 remove cons nil cons "P" 505 ref var 652 remove nil cons cons "x" 504 ref var 625 ref nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 651 remove 647 ref appTerm nil cons cons 145 ref 648 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 643 ref nil cons cons nil cons "P" 650 remove var 647 remove nil cons cons "x" 643 remove var 635 ref nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 645 ref 639 ref appTerm nil cons cons 145 ref 642 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 512 remove cons nil cons 662 def "P" 589 remove var 663 def 639 remove nil cons cons "x" 511 ref var 664 def 641 ref nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 591 remove 611 remove 506 ref 612 ref 615 remove 637 remove 641 ref 614 ref appTerm 665 def appTerm appTerm absTerm appTerm absTerm 666 def appTerm 667 def nil cons cons 145 ref 609 ref cons nil cons 668 def cons nil cons cons 202 ref subst proveHyp nil 663 ref 592 ref 146 ref 666 ref 593 ref appTerm 669 def appTerm 606 ref appTerm 670 def absTerm nil cons cons nil cons nil cons cons 662 ref 23 ref cons 44 ref subst subst 592 remove nil 46 ref 670 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 669 ref nil cons 671 def cons 668 ref cons nil cons cons 672 def 162 ref subst 672 remove 210 ref subst 669 ref betaConv 669 remove assume eqMp nil 144 ref 506 ref 612 ref 363 ref 593 ref 614 ref appTerm appTerm 626 remove 593 ref 636 remove appTerm appTerm 665 remove appTerm appTerm absTerm 673 def appTerm nil cons 674 def cons 675 def 668 remove cons nil cons cons 676 def 202 ref subst proveHyp 676 ref 162 ref subst 676 remove 210 ref subst 604 remove sym nil "P" 504 ref var 677 def 599 remove nil cons cons nil cons nil cons cons 654 ref nil cons 678 def 23 ref cons 44 ref subst 679 def subst 507 ref nil 46 ref 598 remove nil cons cons nil cons nil cons cons 51 ref subst 363 ref refl 680 def nil 612 ref 521 ref nil cons cons nil cons nil cons cons 673 ref 614 ref appTerm 681 def betaConv nil 675 remove 145 ref 681 remove nil cons cons nil cons cons nil cons cons 202 ref subst 678 ref 677 ref 673 remove nil cons cons 612 ref 614 ref nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp subst appThm 597 remove refl appThm sym 680 ref 374 ref refl 682 def 625 remove 521 ref appTerm betaConv 619 ref refl 620 ref 506 ref refl 683 def 531 ref 683 ref 532 ref 621 ref refl 624 remove betaConv 623 remove 401 ref 548 ref appTerm 684 def appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm 549 ref refl 685 def appThm trans appThm 603 ref 635 remove 521 ref appTerm betaConv 628 ref refl 629 ref 683 ref 531 ref 683 ref 532 ref 632 ref refl 634 remove betaConv 633 remove 684 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm 685 ref appThm trans appThm appThm 641 remove 521 ref appTerm betaConv 529 ref refl 686 def 530 ref 683 ref 531 ref 683 ref 532 ref 541 ref refl 687 def 640 remove betaConv 287 ref 287 ref varTerm absTerm 684 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm 685 ref appThm trans appThm appThm 686 remove 530 ref 683 ref 531 ref 683 remove 532 ref 687 remove 596 remove betaConv 595 remove 684 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm 685 remove appThm appThm sym "x" 525 ref var 688 def 97 ref 505 ref constTerm 689 def "a" 503 ref var 690 def 689 ref "b" 503 ref var 691 def 7 ref 0 ref 525 ref 618 ref cons opType constTerm 692 def 688 ref varTerm appTerm 536 remove 690 ref varTerm 693 def appTerm 691 ref varTerm 694 def appTerm 695 def appTerm absTerm appTerm absTerm appTerm absTerm 696 def 549 ref appTerm 697 def betaConv 654 remove "B" 523 remove cons nil cons cons 23 ref cons 698 def nil 25 ref 0 ref 0 ref 522 remove 576 remove opType 699 def 3 ref cons opType 700 def 3 ref cons opType constTerm "x" 699 ref var 701 def 98 ref "a" 26 ref var 702 def 571 remove "b" 565 ref var 703 def 7 ref 0 ref 699 ref 700 remove nil cons cons opType constTerm 701 remove varTerm appTerm 533 remove 0 ref 26 ref 0 ref 565 ref 699 ref nil cons cons opType nil cons cons opType constTerm 702 ref varTerm 704 def appTerm 703 ref varTerm 705 def appTerm 706 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm axiom subst nil 144 ref 25 ref 617 ref constTerm 696 ref appTerm nil cons cons 145 ref 697 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 534 remove cons nil cons "P" 616 ref var 696 remove nil cons cons 688 remove 549 ref nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 689 ref 690 ref 689 ref 691 ref 692 remove 549 ref appTerm 707 def 695 ref appTerm absTerm appTerm absTerm 708 def appTerm 709 def nil cons cons 145 ref 363 ref 374 ref 619 ref 620 remove 506 ref 531 ref 506 ref 532 ref 621 remove 622 ref 543 ref 684 ref appTerm 18 ref appTerm 710 def appTerm 711 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 712 def 549 ref appTerm appTerm 593 ref 628 ref 629 remove 506 ref 531 ref 506 ref 532 ref 632 remove 539 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 713 def 549 ref appTerm appTerm appTerm 529 ref 530 ref 506 ref 531 ref 506 ref 532 ref 541 ref 684 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 714 def 549 ref appTerm appTerm appTerm 529 ref 530 ref 506 ref 531 ref 506 ref 532 ref 541 ref 374 ref 710 ref appTerm 684 ref appTerm 715 def 594 ref appTerm 716 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 717 def 549 ref appTerm appTerm 718 def nil cons 719 def cons nil cons 720 def cons nil cons cons 202 ref subst proveHyp nil 677 ref 531 ref 146 ref 708 ref 537 ref appTerm 721 def appTerm 718 ref appTerm 722 def absTerm nil cons cons nil cons nil cons cons 679 ref subst 531 ref nil 46 ref 722 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 721 ref nil cons 723 def cons 720 ref cons nil cons cons 724 def 162 ref subst 724 remove 210 ref subst 721 ref betaConv 721 remove assume eqMp nil 144 ref 689 remove 691 ref 707 ref 538 remove 694 ref appTerm appTerm absTerm 725 def appTerm 726 def nil cons cons 720 ref cons nil cons cons 202 ref subst proveHyp nil 677 ref 532 ref 146 ref 725 ref 539 ref appTerm 727 def appTerm 718 ref appTerm 728 def absTerm nil cons cons nil cons nil cons cons 679 ref subst 532 ref nil 46 ref 728 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 727 ref nil cons 729 def cons 720 ref cons nil cons cons 730 def 162 ref subst 730 remove 210 ref subst 727 ref betaConv 727 remove assume eqMp nil 144 ref 707 remove 540 ref appTerm 731 def nil cons 732 def cons 720 remove cons nil cons cons 733 def 202 ref subst proveHyp 733 ref 162 ref subst 733 remove 210 ref subst 10 ref "_28646" 525 ref var 734 def 363 ref 374 ref 712 ref 734 remove varTerm 735 def appTerm appTerm 593 ref 713 ref 735 ref appTerm appTerm appTerm 714 ref 735 ref appTerm appTerm appTerm 717 ref 735 remove appTerm appTerm absTerm 736 def 549 ref appTerm 737 def appTerm refl 736 ref 540 ref appTerm betaConv appThm 182 ref 737 remove betaConv appThm 363 ref 374 ref 712 remove 540 ref appTerm appTerm 593 ref 713 remove 540 ref appTerm appTerm appTerm 714 remove 540 ref appTerm appTerm appTerm 717 remove 540 ref appTerm appTerm refl appThm trans 736 remove refl 731 remove assume appThm eqMp sym 680 ref 682 ref 532 ref 10 ref 619 remove "_28658" 616 ref var 738 def 506 ref 531 ref 506 ref 532 ref 10 ref 738 remove varTerm 540 ref appTerm appTerm 711 ref appTerm absTerm appTerm absTerm appTerm absTerm 739 def appTerm 740 def 540 ref appTerm appTerm 711 ref appTerm absTerm 741 def 539 ref appTerm 742 def betaConv 531 ref 506 ref 741 ref appTerm 743 def absTerm 744 def 537 ref appTerm 745 def betaConv 739 ref 740 remove appTerm 746 def betaConv 739 ref "_28656" 525 ref var 747 def 622 ref 543 ref 401 ref 547 ref 628 ref "fn" 627 remove var 748 def 506 ref 690 ref 506 ref 691 ref 631 remove 748 ref varTerm 695 remove appTerm appTerm 749 def 693 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 750 def 747 remove varTerm appTerm appTerm appTerm appTerm 18 ref appTerm appTerm absTerm 751 def appTerm betaConv sym nil 677 ref 531 ref 506 ref 532 ref 10 ref 751 ref 540 ref appTerm 752 def appTerm 711 ref appTerm 753 def absTerm 754 def appTerm 755 def absTerm nil cons cons nil cons nil cons cons 679 ref subst 531 ref nil 46 ref 755 remove nil cons cons nil cons nil cons cons 51 ref subst nil 677 ref 754 remove nil cons cons nil cons nil cons cons 679 ref subst 532 ref nil 46 ref 753 remove nil cons cons nil cons nil cons cons 51 ref subst 752 remove betaConv 10 ref "_28653" 503 ref var 756 def 711 ref absTerm 539 ref appTerm 757 def appTerm refl 756 ref 622 ref 543 ref 401 ref 547 ref 750 ref 540 ref appTerm 758 def appTerm appTerm 759 def appTerm 18 ref appTerm 760 def appTerm 761 def absTerm 762 def 628 remove 748 remove 506 ref 690 ref 506 ref 691 ref 749 remove 694 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 763 def 540 ref appTerm 764 def appTerm betaConv appThm 182 ref 757 remove betaConv appThm 761 remove refl appThm trans 7 ref 0 ref 504 remove 505 remove nil cons cons opType constTerm 765 def "_28652" 503 ref var 766 def 756 remove 622 ref 543 ref 401 ref 547 ref 766 remove varTerm appTerm appTerm appTerm 18 ref appTerm appTerm absTerm absTerm 767 def 537 ref appTerm 768 def appTerm refl 767 ref 758 ref appTerm betaConv appThm 765 remove refl 768 remove betaConv appThm 762 remove refl appThm trans 767 remove refl nil 691 remove 539 ref nil cons 769 def cons 690 remove 537 ref nil cons 770 def cons nil cons cons nil cons cons 771 def 698 ref 703 ref 130 ref 91 ref 0 ref 0 ref 0 ref 699 ref 100 ref cons opType 772 def 3 ref cons opType 773 def 772 ref nil cons 774 def cons opType constTerm "fn" 772 remove var 775 def 29 ref 702 ref 25 ref 570 remove constTerm 776 def 703 ref 130 ref 775 ref varTerm 706 ref appTerm appTerm 777 def 704 ref appTerm absTerm appTerm absTerm appTerm absTerm 778 def appTerm 779 def 706 ref appTerm appTerm 704 ref appTerm absTerm 780 def 705 ref appTerm 781 def betaConv 702 ref 776 ref 780 ref appTerm 782 def absTerm 783 def 704 ref appTerm 784 def betaConv 778 ref 779 remove appTerm 785 def betaConv 97 ref 0 ref 773 ref 3 ref cons opType constTerm 786 def refl 775 remove 29 ref refl 787 def 702 ref 776 ref refl 788 def 703 ref 777 remove refl 702 ref 703 ref 704 ref absTerm 789 def absTerm 790 def 704 ref appTerm betaConv 705 ref refl 791 def appThm 789 remove 705 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 100 ref cons nil cons "_1343" 0 ref 26 ref 0 ref 565 ref 100 remove cons opType nil cons cons opType var 790 remove nil cons cons nil cons nil cons cons nil "f" 0 ref 26 ref 0 ref 565 ref "C" varType 792 def nil cons 793 def cons opType nil cons cons opType 794 def var 795 def 702 ref 703 ref "_1343" 794 ref var varTerm 704 ref appTerm 705 ref appTerm 796 def absTerm 797 def absTerm 798 def nil cons cons nil cons nil cons cons 795 ref 97 ref 0 ref 0 ref 0 ref 699 ref 793 remove cons opType 799 def 3 ref cons opType 800 def 3 ref cons opType 801 def constTerm 802 def "fn" 799 ref var 803 def 29 ref 702 ref 776 ref 703 ref 7 ref 0 ref 792 ref 0 ref 792 remove 3 ref cons opType nil cons cons opType constTerm 803 ref varTerm 804 def 706 ref appTerm appTerm 805 def 795 remove varTerm 806 def 704 ref appTerm 705 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 807 def 806 ref appTerm 808 def betaConv nil 25 ref 0 ref 0 ref 794 ref 3 ref cons opType 809 def 3 ref cons opType constTerm 807 ref appTerm 810 def axiom nil 144 ref 810 remove nil cons cons 145 ref 808 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 794 ref nil cons cons nil cons "P" 809 remove var 807 remove nil cons cons "x" 794 remove var 806 remove nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp subst nil 144 ref 802 ref 803 ref 29 ref 702 ref 776 ref 703 ref 805 ref 798 remove 704 ref appTerm 811 def 705 ref appTerm appTerm absTerm appTerm absTerm appTerm 812 def absTerm 813 def appTerm 814 def nil cons cons 145 ref 802 remove 803 ref 29 ref 702 ref 776 ref 703 ref 805 ref 796 remove appTerm absTerm appTerm absTerm appTerm absTerm 815 def appTerm 816 def nil cons 817 def cons nil cons 818 def cons nil cons cons 202 ref subst nil "P" 800 remove var 819 def 803 ref 146 ref 813 ref 804 ref appTerm 820 def appTerm 816 ref appTerm 821 def absTerm nil cons cons nil cons nil cons cons "A" 799 ref nil cons cons nil cons 822 def 23 ref cons 44 ref subst subst 803 remove nil 46 ref 821 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 820 ref nil cons 823 def cons 818 ref cons nil cons cons 824 def 162 ref subst 824 remove 210 ref subst 820 ref betaConv 820 remove assume eqMp nil 144 ref 812 ref nil cons 825 def cons 818 remove cons nil cons cons 826 def 202 ref subst proveHyp 826 ref 162 ref subst 826 remove 210 ref subst 815 ref 804 ref appTerm betaConv sym 787 ref 702 ref 788 ref 703 ref 805 remove refl 811 remove betaConv 791 ref appThm 797 remove 705 ref appTerm betaConv trans appThm absThm appThm absThm appThm 812 remove assume eqMp eqMp 822 ref 819 ref 815 remove nil cons cons "x" 799 remove var 827 def 804 remove nil cons cons nil cons cons nil cons cons 317 ref subst proveHyp eqMp nil 179 ref 825 remove cons 180 ref 817 remove cons nil cons 828 def cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp nil 179 ref 823 remove cons 828 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp nil 144 ref 25 remove 801 remove constTerm 827 ref 146 ref 813 ref 827 remove varTerm appTerm appTerm 816 ref appTerm absTerm appTerm nil cons cons 145 ref 146 ref 814 remove appTerm 816 remove appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 822 remove 819 remove 813 remove nil cons cons 828 remove cons nil cons cons 332 ref subst eqMp eqMp proveHyp 829 def subst eqMp nil 144 ref 786 remove 778 ref appTerm nil cons cons 145 ref 785 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 774 remove cons nil cons "p" 773 remove var 778 remove nil cons cons nil cons nil cons cons nil 144 ref 228 ref nil cons 830 def cons 831 def 145 ref 10 ref 101 ref appTerm 832 def 36 ref appTerm 833 def nil cons 834 def cons nil cons 835 def cons nil cons cons 836 def 162 ref subst 836 remove 210 ref subst 98 ref refl nil "t" 27 ref var 34 ref nil cons 837 def cons nil cons nil cons cons 203 remove "B" 3 ref cons nil cons cons 23 ref cons "t" 577 ref var 838 def 7 ref 0 ref 577 ref 578 ref nil cons cons opType constTerm 35 ref 838 remove varTerm 839 def 206 ref appTerm absTerm appTerm 839 ref appTerm absTerm 840 def 839 ref appTerm 841 def betaConv nil 658 remove 840 ref appTerm 842 def axiom nil 144 ref 842 remove nil cons cons 145 ref 841 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 577 ref nil cons cons nil cons "P" 578 remove var 840 remove nil cons cons "x" 577 remove var 839 remove nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp subst subst appThm nil 46 ref 830 ref cons nil cons nil cons cons 843 def 51 ref subst 228 ref assume eqMp trans sym 50 ref eqMp nil 144 ref 98 ref 35 ref 229 ref absTerm appTerm nil cons cons 835 ref cons nil cons cons 202 ref subst proveHyp nil 30 ref 837 ref cons 180 ref 834 remove cons nil cons 844 def cons nil cons cons nil 305 remove 145 ref 146 ref 98 remove 35 ref 207 ref absTerm 845 def appTerm 846 def appTerm 185 ref appTerm 847 def nil cons 848 def cons nil cons 849 def cons nil cons cons 850 def 239 remove nil 144 ref 235 ref cons 851 def 145 ref 146 ref 149 ref appTerm 852 def 147 ref appTerm nil cons 853 def cons nil cons 854 def cons nil cons cons 210 ref subst proveHyp 852 ref refl 238 remove appThm sym nil 144 ref 176 ref cons 855 def 145 ref 176 ref cons nil cons 856 def cons nil cons cons 857 def 162 ref subst 857 remove 210 ref subst 177 remove eqMp nil 179 ref 176 remove cons 181 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp 858 def eqMp nil 855 ref 145 ref 174 ref cons nil cons 859 def cons nil cons cons 202 ref subst nil 179 ref 235 remove cons 860 def 180 ref 853 remove cons nil cons 861 def cons nil cons cons 862 def 285 remove subst eqMp 202 ref 862 remove 194 ref subst eqMp deductAntisym deductAntisym 863 def subst 850 ref 162 ref subst 850 remove 210 ref subst nil 30 ref 35 ref 146 ref 845 ref 206 ref appTerm 864 def appTerm 185 ref appTerm 865 def absTerm 866 def nil cons cons nil cons nil cons cons 44 ref subst 35 ref nil 46 ref 865 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 864 ref nil cons 867 def cons 307 ref cons nil cons cons 868 def 162 ref subst 868 remove 210 ref subst 864 ref betaConv 869 def 864 remove assume eqMp 310 remove proveHyp 314 remove eqMp eqMp nil 179 ref 867 remove cons 316 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp nil 144 ref 29 ref 866 remove appTerm nil cons cons 849 remove cons nil cons cons 202 ref subst proveHyp 204 ref 30 ref 845 remove nil cons cons 870 def 316 ref cons nil cons cons 332 ref subst eqMp eqMp nil 315 remove 180 ref 848 ref cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp nil 144 ref 300 remove 847 ref appTerm nil cons cons 145 ref 146 ref 847 ref appTerm 299 remove appTerm nil cons cons nil cons cons nil cons cons 210 ref subst proveHyp nil 144 ref 848 ref cons 145 ref 304 ref cons nil cons cons nil cons cons 871 def 162 ref subst 871 remove 210 ref subst nil 312 remove nil cons nil cons cons 44 ref subst 35 ref nil 46 ref 297 remove nil cons cons nil cons nil cons cons 51 ref subst 309 ref 162 ref subst 309 remove 210 ref subst 869 remove sym 207 remove assume eqMp 204 ref 870 remove 313 ref cons nil cons cons 317 ref subst proveHyp nil 144 ref 846 remove nil cons cons 307 remove cons nil cons cons 202 ref subst 847 remove assume eqMp proveHyp eqMp nil 179 ref 208 remove cons 316 remove cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 179 ref 848 remove cons 180 ref 304 remove cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp subst nil 30 ref 35 ref 292 ref 833 ref appTerm 872 def absTerm nil cons cons nil cons nil cons cons 44 remove subst 35 ref nil 46 ref 872 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 229 remove nil cons 873 def cons 874 def 835 remove cons nil cons cons 875 def 162 ref subst 875 remove 210 ref subst nil 46 ref 101 ref nil cons 876 def cons nil cons nil cons cons 51 ref subst nil 874 remove 145 ref 876 remove cons 877 def nil cons cons nil cons cons 202 ref subst 35 ref 292 remove 101 ref appTerm absTerm 878 def 206 ref appTerm 879 def betaConv 33 remove 29 ref 878 ref appTerm 880 def absTerm 881 def 34 remove appTerm 882 def betaConv nil 655 remove 881 ref appTerm 883 def axiom nil 144 ref 883 remove nil cons cons 145 ref 882 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 129 remove cons nil cons "P" 28 remove var 881 remove nil cons cons "x" 27 remove var 837 remove cons nil cons cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 880 remove nil cons cons 145 ref 879 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 204 ref 30 ref 878 remove nil cons cons 313 remove cons nil cons cons 212 ref subst eqMp eqMp eqMp eqMp eqMp nil 179 ref 873 remove cons 844 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp eqMp eqMp nil 179 ref 830 ref cons 844 remove cons nil cons cons 194 ref subst deductAntisym eqMp nil 144 ref 146 ref 228 ref appTerm 884 def 833 remove appTerm nil cons cons 145 ref 10 ref 884 ref 101 remove appTerm appTerm 885 def 884 ref 36 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp nil "q'" 2 ref var 886 def 36 ref nil cons cons nil cons nil cons cons 228 ref refl nil 144 ref 10 ref 228 ref appTerm 887 def 228 remove appTerm nil cons cons 145 ref 146 ref 884 ref 832 remove 886 ref varTerm 888 def appTerm 889 def appTerm appTerm 885 ref 884 remove 888 ref appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp nil "p'" 2 ref var 890 def 830 remove cons nil cons nil cons cons 886 ref 146 ref 887 remove 890 ref varTerm 891 def appTerm appTerm 146 ref 146 ref 891 ref appTerm 892 def 889 remove appTerm appTerm 885 remove 892 ref 888 ref appTerm 893 def appTerm appTerm appTerm absTerm 894 def 888 ref appTerm 895 def betaConv 890 ref 291 ref 894 ref appTerm 896 def absTerm 897 def 891 ref appTerm 898 def betaConv nil 877 remove 831 remove nil cons cons nil cons cons nil 295 ref 890 ref 291 ref 886 ref 146 ref 231 remove 891 ref appTerm 899 def appTerm 146 ref 892 ref 10 ref 149 ref appTerm 888 ref appTerm 900 def appTerm 901 def appTerm 151 remove 893 ref appTerm 902 def appTerm 903 def appTerm 904 def absTerm 905 def appTerm 906 def absTerm nil cons cons nil cons nil cons cons 303 ref subst 890 remove nil 46 ref 906 remove nil cons cons nil cons nil cons cons 51 ref subst nil 295 ref 905 remove nil cons cons nil cons nil cons cons 303 ref subst 886 remove nil 46 ref 904 remove nil cons cons nil cons nil cons cons 51 ref subst nil 144 ref 899 remove nil cons 907 def cons 908 def 145 ref 903 remove nil cons 909 def cons nil cons cons nil cons cons 910 def 162 ref subst 910 remove 210 ref subst nil 144 ref 901 ref nil cons 911 def cons 145 ref 902 remove nil cons 912 def cons nil cons cons nil cons cons 913 def 162 ref subst 913 remove 210 ref subst nil 851 remove 145 ref 893 ref nil cons 914 def cons nil cons cons nil cons cons 915 def 863 remove subst 915 ref 162 ref subst 915 remove 210 ref subst nil 144 ref 891 ref nil cons 916 def cons 917 def 145 ref 888 ref nil cons 918 def cons nil cons 919 def cons nil cons cons 920 def 162 ref subst 920 ref 210 ref subst nil 908 ref 145 ref 148 ref 891 remove appTerm 921 def nil cons 922 def cons nil cons cons nil cons cons 202 ref subst nil 144 ref 174 remove cons 145 ref 916 ref cons nil cons cons nil cons cons 923 def 242 ref subst eqMp 924 def nil 144 ref 922 ref cons 925 def 919 ref cons nil cons cons 926 def 202 ref subst proveHyp nil 908 remove 145 ref 892 remove 147 remove appTerm 927 def nil cons 928 def cons nil cons cons nil cons cons 202 ref subst 923 ref nil 234 remove 854 remove cons nil cons cons 929 def 162 ref subst 929 remove 210 ref subst 858 remove eqMp nil 240 remove 861 remove cons nil cons cons 194 ref subst deductAntisym eqMp 930 def subst eqMp 931 def nil 144 ref 928 ref cons 932 def 145 ref 146 ref 921 ref appTerm 933 def 888 ref appTerm nil cons 934 def cons nil cons cons nil cons cons 935 def 202 ref subst proveHyp 935 ref 162 ref subst 935 remove 210 ref subst 926 ref 162 ref subst 926 remove 210 ref subst nil 917 ref 859 remove cons nil cons cons 202 ref subst 927 remove assume eqMp 936 def 923 remove 202 ref subst 921 remove assume eqMp 937 def 936 remove proveHyp proveHyp nil 917 remove 145 ref 900 remove nil cons 938 def cons nil cons cons nil cons cons 202 ref subst 901 remove assume eqMp 939 def nil 144 ref 938 remove cons 940 def 145 ref 852 ref 888 ref appTerm 941 def nil cons 942 def cons nil cons cons nil cons cons 202 ref subst proveHyp nil 855 remove 919 ref cons nil cons cons 943 def 242 remove subst eqMp 944 def nil 144 ref 942 ref cons 945 def 919 remove cons nil cons cons 946 def 202 ref subst proveHyp 939 remove nil 940 remove 145 ref 146 ref 888 ref appTerm 149 ref appTerm 947 def nil cons 948 def cons nil cons cons nil cons cons 202 ref subst proveHyp 943 ref 930 remove subst eqMp 949 def nil 144 ref 948 ref cons 950 def 145 ref 146 ref 941 ref appTerm 951 def 888 remove appTerm nil cons 952 def cons nil cons cons nil cons cons 953 def 202 ref subst proveHyp 953 ref 162 ref subst 953 remove 210 ref subst 946 ref 162 ref subst 946 remove 210 ref subst 201 remove 943 remove 202 ref subst 941 remove assume eqMp proveHyp eqMp nil 179 ref 942 remove cons 954 def 180 ref 918 ref cons nil cons 955 def cons nil cons cons 194 ref subst deductAntisym eqMp eqMp nil 179 ref 948 remove cons 956 def 180 ref 952 remove cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 179 ref 922 remove cons 957 def 955 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp nil 179 ref 928 remove cons 958 def 180 ref 934 remove cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 179 ref 916 ref cons 955 remove cons nil cons cons 194 ref subst deductAntisym eqMp eqMp nil 860 remove 180 ref 914 ref cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp nil 144 ref 146 ref 150 ref appTerm 893 ref appTerm nil cons cons 145 ref 146 ref 893 ref appTerm 150 remove appTerm nil cons cons nil cons cons nil cons cons 210 ref subst proveHyp nil 144 ref 914 ref cons 236 remove cons nil cons cons 959 def 162 ref subst 959 remove 210 ref subst 162 ref 210 ref 924 remove nil 925 remove 856 ref cons nil cons cons 960 def 202 ref subst proveHyp 931 remove nil 932 remove 145 ref 933 remove 149 ref appTerm nil cons 961 def cons nil cons cons nil cons cons 962 def 202 ref subst proveHyp 962 ref 162 ref subst 962 remove 210 ref subst 960 ref 162 ref subst 960 remove 210 ref subst 937 remove 944 remove nil 945 remove 856 ref cons nil cons cons 963 def 202 ref subst proveHyp 949 remove nil 950 remove 145 ref 951 remove 149 ref appTerm nil cons 964 def cons nil cons cons nil cons cons 965 def 202 ref subst proveHyp 965 ref 162 ref subst 965 remove 210 ref subst 963 ref 162 ref subst 963 remove 210 ref subst 920 remove 202 ref subst 893 remove assume eqMp nil 144 ref 918 ref cons 856 remove cons nil cons cons 202 ref subst 947 remove assume eqMp proveHyp eqMp nil 954 remove 181 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp nil 956 remove 180 ref 964 remove cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 957 remove 181 remove cons nil cons cons 194 ref subst deductAntisym eqMp eqMp nil 958 remove 180 ref 961 remove cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp eqMp 195 remove deductAntisym eqMp eqMp nil 179 ref 914 remove cons 241 remove cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 179 ref 911 remove cons 180 ref 912 remove cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp eqMp nil 179 ref 907 remove cons 180 ref 909 remove cons nil cons cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp subst nil 144 ref 291 ref 897 ref appTerm nil cons cons 145 ref 898 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 302 ref 295 ref 897 remove nil cons cons 331 ref 916 remove cons nil cons cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 896 remove nil cons cons 145 ref 895 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 302 ref 295 ref 894 remove nil cons cons 331 ref 918 remove cons nil cons cons nil cons cons 212 ref subst eqMp eqMp subst eqMp subst eqMp 843 remove 46 ref 10 ref 146 ref 47 ref appTerm 36 ref appTerm appTerm 36 ref appTerm absTerm 966 def 47 ref appTerm 967 def betaConv nil 291 ref 966 ref appTerm 968 def axiom nil 144 ref 968 remove nil cons cons 145 ref 967 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 302 ref 295 ref 966 remove nil cons cons 331 ref 47 remove nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp subst trans sym 50 ref eqMp 969 def subst eqMp eqMp nil 144 ref 29 ref 783 ref appTerm nil cons cons 145 ref 784 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 204 ref 30 ref 783 remove nil cons cons 35 ref 704 ref nil cons cons nil cons 970 def cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 782 remove nil cons cons 145 ref 781 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 575 ref cons nil cons 971 def "P" 566 remove var 972 def 780 remove nil cons cons "x" 565 remove var 705 ref nil cons cons nil cons 973 def cons nil cons cons 212 ref subst eqMp eqMp sym subst subst 974 def appThm eqMp 771 remove 698 remove 703 ref 660 ref 91 remove 0 ref 0 ref 0 ref 699 remove 575 ref cons opType 975 def 3 ref cons opType 976 def 975 ref nil cons 977 def cons opType constTerm "fn" 975 remove var 978 def 29 ref 702 ref 776 ref 703 ref 660 remove 978 ref varTerm 706 ref appTerm appTerm 979 def 705 ref appTerm absTerm appTerm absTerm appTerm absTerm 980 def appTerm 981 def 706 remove appTerm appTerm 705 ref appTerm absTerm 982 def 705 ref appTerm 983 def betaConv 702 ref 776 remove 982 ref appTerm 984 def absTerm 985 def 704 ref appTerm 986 def betaConv 980 ref 981 remove appTerm 987 def betaConv 97 ref 0 ref 976 ref 3 ref cons opType constTerm 988 def refl 978 remove 787 remove 702 ref 788 remove 703 ref 979 remove refl 702 remove 703 remove 705 ref absTerm 989 def absTerm 990 def 704 remove appTerm betaConv 791 remove appThm 989 remove 705 remove appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 575 remove cons nil cons "_1343" 0 ref 26 ref 661 remove cons opType var 990 remove nil cons cons nil cons nil cons cons 829 remove subst eqMp nil 144 ref 988 remove 980 ref appTerm nil cons cons 145 ref 987 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp "A" 977 remove cons nil cons "p" 976 remove var 980 remove nil cons cons nil cons nil cons cons 969 ref subst eqMp eqMp nil 144 ref 29 ref 985 ref appTerm nil cons cons 145 ref 986 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 204 ref 30 ref 985 remove nil cons cons 970 remove cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 984 remove nil cons cons 145 ref 983 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 971 remove 972 remove 982 remove nil cons cons 973 remove cons nil cons cons 212 ref subst eqMp eqMp sym subst subst 991 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 618 remove cons nil cons 992 def "P" 617 ref var 739 ref nil cons 993 def cons "x" 616 remove var 751 remove nil cons cons nil cons cons nil cons cons 317 ref subst proveHyp nil 144 ref 97 ref 0 ref 617 ref 3 ref cons opType constTerm 739 remove appTerm nil cons cons 145 ref 746 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp nil "p" 617 remove var 993 remove cons nil cons nil cons cons 992 remove 23 ref cons 969 ref subst subst eqMp eqMp nil 144 ref 506 ref 744 ref appTerm nil cons cons 145 ref 745 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 678 ref 677 ref 744 remove nil cons cons 612 ref 770 remove cons nil cons 994 def cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 743 remove nil cons cons 145 ref 742 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 678 ref 677 ref 741 remove nil cons cons 612 ref 769 remove cons nil cons 995 def cons nil cons cons 212 ref subst eqMp eqMp appThm 603 remove 991 ref sym appThm appThm 532 ref 363 ref 529 ref "_28682" 526 ref var 996 def 506 ref 531 ref 506 ref 532 ref 363 ref 996 remove varTerm 540 ref appTerm appTerm 684 ref appTerm absTerm appTerm absTerm appTerm absTerm 997 def appTerm 998 def 540 ref appTerm appTerm 684 ref appTerm absTerm 999 def 539 ref appTerm 1000 def betaConv 531 ref 506 ref 999 ref appTerm 1001 def absTerm 1002 def 537 ref appTerm 1003 def betaConv 997 ref 998 remove appTerm 1004 def betaConv 997 ref "_28680" 525 ref var 1005 def 401 ref 547 ref 750 ref 1005 remove varTerm appTerm appTerm appTerm absTerm 1006 def appTerm betaConv sym nil 677 ref 531 ref 506 ref 532 ref 363 ref 1006 ref 540 ref appTerm 1007 def appTerm 684 ref appTerm 1008 def absTerm 1009 def appTerm 1010 def absTerm nil cons cons nil cons nil cons cons 679 ref subst 531 ref nil 46 ref 1010 remove nil cons cons nil cons nil cons cons 51 ref subst nil 677 ref 1009 remove nil cons cons nil cons nil cons cons 679 ref subst 532 ref nil 46 ref 1008 remove nil cons cons nil cons nil cons cons 51 ref subst 1007 remove betaConv 363 ref "_28677" 503 ref var 1011 def 684 ref absTerm 539 ref appTerm 1012 def appTerm refl 1011 ref 759 ref absTerm 1013 def 764 ref appTerm betaConv appThm 680 ref 1012 remove betaConv appThm 759 ref refl appThm trans 7 remove 0 ref 511 remove 605 remove cons opType constTerm 1014 def "_28676" 503 ref var 1015 def 1011 remove 401 ref 547 ref 1015 remove varTerm appTerm appTerm absTerm absTerm 1016 def 537 ref appTerm 1017 def appTerm refl 1016 ref 758 ref appTerm betaConv appThm 1014 ref refl 1018 def 1017 remove betaConv appThm 1013 remove refl appThm trans 1016 remove refl 974 ref appThm eqMp 991 ref appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 528 remove cons nil cons 1019 def "P" 527 ref var 1020 def 997 ref nil cons 1021 def cons "x" 526 ref var 1022 def 1006 remove nil cons cons nil cons cons nil cons cons 317 ref subst proveHyp nil 144 ref 97 remove 0 ref 527 ref 3 remove cons opType constTerm 1023 def 997 remove appTerm nil cons cons 145 ref 1004 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp nil "p" 527 remove var 1024 def 1021 remove cons nil cons nil cons cons 1019 ref 23 remove cons 969 remove subst 1025 def subst eqMp eqMp nil 144 ref 506 ref 1002 ref appTerm nil cons cons 145 ref 1003 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 678 ref 677 ref 1002 remove nil cons cons 994 ref cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 1001 remove nil cons cons 145 ref 1000 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 678 ref 677 ref 999 remove nil cons cons 995 ref cons nil cons cons 212 ref subst eqMp eqMp appThm appThm 532 ref 363 ref 529 ref "_28694" 526 remove var 1026 def 506 ref 531 ref 506 ref 532 ref 363 ref 1026 remove varTerm 540 ref appTerm appTerm 716 ref appTerm absTerm appTerm absTerm appTerm absTerm 1027 def appTerm 1028 def 540 ref appTerm appTerm 716 ref appTerm absTerm 1029 def 539 ref appTerm 1030 def betaConv 531 ref 506 ref 1029 ref appTerm 1031 def absTerm 1032 def 537 ref appTerm 1033 def betaConv 1027 ref 1028 remove appTerm 1034 def betaConv 1027 ref "_28692" 525 remove var 1035 def 374 ref 543 ref 401 ref 547 ref 750 remove 1035 remove varTerm 1036 def appTerm appTerm appTerm 1037 def appTerm 18 ref appTerm appTerm 1037 remove appTerm 593 ref 763 remove 1036 remove appTerm appTerm appTerm absTerm 1038 def appTerm betaConv sym nil 677 ref 531 ref 506 ref 532 ref 363 ref 1038 ref 540 remove appTerm 1039 def appTerm 716 ref appTerm 1040 def absTerm 1041 def appTerm 1042 def absTerm nil cons cons nil cons nil cons cons 679 ref subst 531 ref nil 46 ref 1042 remove nil cons cons nil cons nil cons cons 51 ref subst nil 677 ref 1041 remove nil cons cons nil cons nil cons cons 679 ref subst 532 ref nil 46 ref 1040 remove nil cons cons nil cons nil cons cons 51 ref subst 1039 remove betaConv 363 ref "_28689" 503 ref var 1043 def 715 remove 593 ref 1043 ref varTerm appTerm 1044 def appTerm absTerm 539 ref appTerm 1045 def appTerm refl 1043 ref 374 ref 760 remove appTerm 759 remove appTerm 1046 def 1044 ref appTerm absTerm 1047 def 764 ref appTerm betaConv appThm 680 ref 1045 remove betaConv appThm 1046 remove 593 ref 764 remove appTerm appTerm refl appThm trans 1014 remove "_28688" 503 remove var 1048 def 1043 remove 374 ref 543 ref 401 ref 547 remove 1048 remove varTerm appTerm appTerm 1049 def appTerm 18 ref appTerm appTerm 1049 remove appTerm 1044 remove appTerm absTerm absTerm 1050 def 537 remove appTerm 1051 def appTerm refl 1050 ref 758 remove appTerm betaConv appThm 1018 remove 1051 remove betaConv appThm 1047 remove refl appThm trans 1050 remove refl 974 remove appThm eqMp 991 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 1019 remove 1020 remove 1027 ref nil cons 1052 def cons 1022 remove 1038 remove nil cons cons nil cons cons nil cons cons 317 ref subst proveHyp nil 144 ref 1023 remove 1027 remove appTerm nil cons cons 145 ref 1034 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp nil 1024 remove 1052 remove cons nil cons nil cons cons 1025 remove subst eqMp eqMp nil 144 ref 506 ref 1032 ref appTerm nil cons cons 145 ref 1033 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 678 ref 677 ref 1032 remove nil cons cons 994 remove cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 1031 remove nil cons cons 145 ref 1030 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 678 ref 677 ref 1029 remove nil cons cons 995 remove cons nil cons cons 212 ref subst eqMp eqMp appThm sym nil 144 ref 10 ref 710 ref appTerm 1053 def "Data.Bool.F" const 2 ref constTerm 1054 def appTerm 1055 def nil cons 1056 def cons 145 ref 363 ref 374 ref 711 remove appTerm 594 ref appTerm 684 ref appTerm appTerm 716 remove appTerm nil cons 1057 def cons nil cons 1058 def cons nil cons cons 1059 def 162 ref subst 1059 remove 210 ref subst 10 ref "_28698" 2 ref var 1060 def 363 ref 374 ref 622 ref 1060 remove varTerm 1061 def appTerm appTerm 594 ref appTerm 684 ref appTerm appTerm 374 ref 1061 remove appTerm 684 ref appTerm 594 ref appTerm appTerm absTerm 1062 def 710 ref appTerm 1063 def appTerm refl 1064 def 1062 ref 1054 ref appTerm betaConv appThm 182 remove 1063 remove betaConv appThm 1065 def 363 ref 374 ref 622 ref 1054 ref appTerm 1066 def appTerm 594 ref appTerm 684 ref appTerm appTerm 374 ref 1054 ref appTerm 684 ref appTerm 594 ref appTerm appTerm refl appThm trans 1062 remove refl 1067 def 1055 remove assume appThm eqMp sym 680 ref 682 ref nil 10 ref 1066 remove appTerm 36 ref appTerm axiom appThm 594 ref refl 1068 def appThm 684 ref refl 1069 def appThm nil "t2" 1 ref var 1070 def 684 ref nil cons 1071 def cons "t1" 1 ref var 1072 def 594 ref nil cons 1073 def cons nil cons cons nil cons cons 1074 def 24 ref "t2" 26 ref var 1075 def 130 ref 373 ref 0 ref 2 ref 0 ref 26 ref 656 remove nil cons cons opType nil cons cons opType constTerm 1076 def 36 ref appTerm "t1" 26 remove var 1077 def varTerm 1078 def appTerm 1075 ref varTerm 1079 def appTerm appTerm 1078 ref appTerm absTerm 1080 def 1079 ref appTerm 1081 def betaConv 1077 ref 29 ref 1080 ref appTerm 1082 def absTerm 1083 def 1078 ref appTerm 1084 def betaConv nil 29 ref 1083 ref appTerm 1085 def axiom nil 144 ref 1085 remove nil cons cons 145 ref 1084 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 204 ref 30 ref 1083 remove nil cons cons 35 ref 1078 ref nil cons cons nil cons 1086 def cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 1082 remove nil cons cons 145 ref 1081 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 204 ref 30 ref 1080 remove nil cons cons 35 remove 1079 ref nil cons cons nil cons 1087 def cons nil cons cons 212 ref subst eqMp eqMp subst 1088 def subst trans appThm nil 1070 remove 1073 ref cons 1072 remove 1071 ref cons nil cons cons nil cons cons 1089 def 24 ref 1075 remove 130 remove 1076 remove 1054 ref appTerm 1078 ref appTerm 1079 ref appTerm appTerm 1079 ref appTerm absTerm 1090 def 1079 remove appTerm 1091 def betaConv 1077 remove 29 ref 1090 ref appTerm 1092 def absTerm 1093 def 1078 remove appTerm 1094 def betaConv nil 29 remove 1093 ref appTerm 1095 def axiom nil 144 ref 1095 remove nil cons cons 145 ref 1094 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 204 ref 30 ref 1093 remove nil cons cons 1086 remove cons nil cons cons 212 ref subst eqMp eqMp nil 144 ref 1092 remove nil cons cons 145 ref 1091 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 204 remove 30 remove 1090 remove nil cons cons 1087 remove cons nil cons cons 212 ref subst eqMp eqMp subst 1096 def subst appThm nil 287 ref 1073 remove cons nil cons nil cons cons 24 remove nil 46 ref 222 remove 206 remove appTerm nil cons cons nil cons nil cons cons 51 ref subst 211 remove eqMp subst 1097 def subst trans sym 50 ref eqMp eqMp eqMp nil 179 ref 1056 ref cons 180 ref 1057 ref cons nil cons 1098 def cons nil cons cons 194 ref subst deductAntisym eqMp nil 144 ref 1053 remove 36 ref appTerm 1099 def nil cons 1100 def cons 1058 remove cons nil cons cons 1101 def 162 remove subst 1101 remove 210 remove subst 1064 remove "_28696" 2 ref var 1102 def 363 ref 374 ref 622 ref 1102 remove varTerm 1103 def appTerm appTerm 594 ref appTerm 684 ref appTerm appTerm 374 ref 1103 remove appTerm 684 ref appTerm 594 ref appTerm appTerm absTerm 36 ref appTerm betaConv appThm 1065 remove 363 ref 374 ref 622 remove 36 ref appTerm 1104 def appTerm 594 ref appTerm 684 ref appTerm appTerm 374 ref 36 remove appTerm 684 remove appTerm 594 remove appTerm appTerm refl appThm trans 1067 remove 1099 remove assume appThm eqMp sym 680 remove 682 remove nil 10 ref 1104 remove appTerm 1054 ref appTerm axiom appThm 1068 remove appThm 1069 remove appThm 1074 remove 1096 remove subst trans appThm 1089 remove 1088 remove subst appThm nil 287 remove 1071 remove cons nil cons nil cons cons 1097 remove subst trans sym 50 remove eqMp eqMp eqMp nil 179 ref 1100 remove cons 1105 def 1098 remove cons nil cons cons 194 ref subst deductAntisym eqMp 46 ref 429 ref 49 remove appTerm 48 remove 1054 remove appTerm appTerm absTerm 1106 def 710 ref appTerm 1107 def betaConv nil 291 ref 1106 ref appTerm 1108 def axiom nil 144 ref 1108 remove nil cons cons 145 ref 1107 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 302 ref 295 ref 1106 remove nil cons cons 331 ref 710 remove nil cons cons nil cons cons nil cons cons 212 ref subst eqMp eqMp nil 1105 remove 180 ref 1056 remove cons "R" 2 ref var 1109 def 1057 remove cons nil cons cons cons nil cons cons nil 144 ref 146 ref 185 ref appTerm 1110 def 1109 remove varTerm 1111 def appTerm 1112 def nil cons cons 145 ref 1111 ref nil cons 1113 def cons nil cons cons nil cons cons 202 ref subst nil 144 ref 146 ref 183 ref appTerm 1114 def 1111 ref appTerm nil cons cons 145 ref 146 ref 1112 remove appTerm 1111 ref appTerm nil cons cons nil cons cons nil cons cons 202 ref subst "r" 2 ref var 1115 def 146 ref 1114 remove 1115 ref varTerm 1116 def appTerm appTerm 1117 def 146 ref 1110 remove 1116 ref appTerm appTerm 1116 ref appTerm appTerm absTerm 1118 def 1111 remove appTerm 1119 def betaConv 10 ref 429 ref 183 ref appTerm 1120 def 185 ref appTerm 1121 def appTerm refl 145 ref 291 ref 1115 ref 1117 remove 146 ref 852 remove 1116 ref appTerm appTerm 1116 ref appTerm 1122 def appTerm absTerm appTerm absTerm 185 remove appTerm betaConv appThm 170 remove 1120 remove appTerm refl 144 ref 145 ref 291 ref 1115 remove 146 ref 148 remove 1116 remove appTerm appTerm 1122 remove appTerm absTerm appTerm absTerm absTerm 1123 def 183 remove appTerm betaConv appThm nil 159 remove 429 ref appTerm 1123 remove appTerm axiom 192 remove appThm eqMp 188 remove appThm eqMp 1121 remove assume eqMp nil 144 ref 291 ref 1118 ref appTerm nil cons cons 145 ref 1119 remove nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 302 remove 295 ref 1118 remove nil cons cons 331 remove 1113 remove cons nil cons cons nil cons cons 212 remove subst eqMp eqMp eqMp eqMp subst proveHyp proveHyp proveHyp eqMp eqMp eqMp nil 179 ref 732 remove cons 180 ref 719 remove cons nil cons 1124 def cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp nil 179 ref 729 remove cons 1124 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp nil 144 ref 506 ref 612 ref 146 ref 725 ref 614 ref appTerm appTerm 718 ref appTerm absTerm appTerm nil cons cons 145 ref 146 ref 726 remove appTerm 718 ref appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 678 ref 677 ref 725 remove nil cons cons 1124 ref cons nil cons cons 332 ref subst eqMp eqMp eqMp nil 179 ref 723 remove cons 1124 ref cons nil cons cons 194 ref subst deductAntisym eqMp eqMp absThm eqMp nil 144 ref 506 ref 612 remove 146 ref 708 ref 614 remove appTerm appTerm 718 ref appTerm absTerm appTerm nil cons cons 145 ref 146 ref 709 remove appTerm 718 remove appTerm nil cons cons nil cons cons nil cons cons 202 ref subst proveHyp 678 remove 677 ref 708 remove nil cons cons 1124 remove cons nil cons cons 332 ref subst eqMp eqMp eqMp eqMp eqMp absThm eqMp eqMp 662 ref 663 ref 600 remove nil cons cons 664 ref 593 remove nil cons cons nil cons cons nil cons cons 317 remove subst proveHyp eqMp nil 179 ref 674 remove cons 180 remove 609 remove cons nil cons 1125 def cons nil cons cons 194 ref subst deductAntisym eqMp eqMp eqMp nil 179 remove 671 remove cons 1125 ref cons nil cons cons 194 remove subst deductAntisym eqMp eqMp absThm eqMp nil 144 remove 645 remove 664 ref 146 ref 666 ref 664 remove varTerm appTerm appTerm 606 ref appTerm absTerm appTerm nil cons cons 145 ref 146 remove 667 remove appTerm 606 remove appTerm nil cons cons nil cons cons nil cons cons 202 remove subst proveHyp 662 remove 663 remove 666 remove nil cons cons 1125 remove cons nil cons cons 332 remove subst eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp eqMp eqMp eqMp defineConstList 1126 def pop hdTl pop 515 remove constTerm 1127 def 508 ref varTerm 1128 def appTerm 519 ref appTerm 509 ref varTerm 1129 def appTerm absTerm 416 ref "Number.Natural.-" const 76 ref constTerm 1130 def 1128 ref appTerm 79 ref appTerm appTerm appTerm 1131 def absTerm 1132 def absTerm 1133 def defineConst 1134 def pop 513 remove constTerm 1135 def 18 ref appTerm 521 ref appTerm appTerm 510 ref 1127 remove 18 ref appTerm 519 remove appTerm 1136 def 521 remove appTerm 1137 def absTerm 416 ref 1130 remove 18 ref appTerm 79 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm 1138 def nil cons cons nil cons nil cons cons 45 ref subst 508 remove nil 46 ref 506 ref 509 ref 363 ref 1135 remove 1128 ref appTerm 1129 ref appTerm appTerm 1131 remove appTerm 1139 def absTerm 1140 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 677 remove 1140 remove nil cons cons nil cons nil cons cons 679 remove subst 509 remove nil 46 ref 1139 remove nil cons cons nil cons nil cons cons 51 ref subst 1134 remove 1128 ref refl appThm 1133 remove 1128 remove appTerm betaConv trans 1129 ref refl appThm 1132 remove 1129 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 52 ref 1138 remove appTerm thm nil 295 remove 145 remove 52 ref 542 ref 52 ref 6 ref 10 ref "Number.Natural.Bits.compare" "_28568" 2 ref var 1141 def "_28569" 1 ref var 1142 def "_28570" 1 ref var 1143 def 373 remove 0 ref 2 ref 9 remove nil cons cons opType constTerm 1144 def 1141 ref varTerm 1145 def appTerm "Number.Natural.<=" const 362 ref constTerm 1146 def 1142 ref varTerm 1147 def appTerm 1143 ref varTerm 1148 def appTerm appTerm 543 remove 1147 ref appTerm 1148 ref appTerm appTerm 1149 def absTerm 1150 def absTerm 1151 def absTerm 1152 def defineConst 1153 def pop 0 ref 2 remove 362 remove nil cons cons opType constTerm 1154 def 149 ref appTerm 544 ref appTerm 18 ref appTerm appTerm 1144 remove 149 remove appTerm 1146 remove 544 ref appTerm 18 ref appTerm appTerm 545 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm 1155 def nil cons cons nil cons nil cons cons 303 remove subst 1141 remove nil 46 ref 52 ref 1142 ref 52 ref 1143 ref 10 remove 1154 remove 1145 ref appTerm 1147 ref appTerm 1148 ref appTerm appTerm 1149 remove appTerm 1156 def absTerm 1157 def appTerm 1158 def absTerm 1159 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 1159 remove nil cons cons nil cons nil cons cons 45 ref subst 1142 remove nil 46 ref 1158 remove nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 1157 remove nil cons cons nil cons nil cons cons 45 ref subst 1143 remove nil 46 ref 1156 remove nil cons cons nil cons nil cons cons 51 ref subst 1153 remove 1145 ref refl appThm 1152 remove 1145 remove appTerm betaConv trans 1147 ref refl appThm 1151 remove 1147 remove appTerm betaConv trans 1148 ref refl appThm 1150 remove 1148 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 291 remove 1155 remove appTerm thm nil 5 ref 6 ref 363 ref 421 ref appTerm 374 remove 363 ref 18 ref appTerm 65 ref appTerm appTerm 65 ref appTerm 371 remove 412 remove 18 ref appTerm appTerm 79 remove appTerm appTerm appTerm absTerm 1160 def nil cons cons nil cons nil cons cons 45 ref subst 410 remove nil 46 ref 363 ref 416 ref 411 ref appTerm appTerm 413 remove appTerm nil cons cons nil cons nil cons cons 51 ref subst 415 remove 411 ref refl appThm 414 remove 411 remove appTerm betaConv trans eqMp absThm eqMp nil 52 ref 1160 remove appTerm thm nil 5 ref 542 ref 52 ref 6 ref 363 ref "Number.Natural.Bits.and" "_28622" 1 ref var 1161 def "_28623" 1 ref var 1162 def 401 ref "Data.List.map" const 0 ref 4 remove 0 ref 53 remove 21 remove opType 1163 def 55 remove cons opType nil cons cons opType constTerm 1164 def 438 ref 60 ref 457 ref 1161 ref varTerm 1165 def appTerm 458 ref appTerm appTerm 457 ref 1162 ref varTerm 1166 def appTerm 458 ref appTerm appTerm absTerm appTerm "Data.List.interval" const 0 ref 1 ref 0 remove 1 ref 1163 remove nil cons cons opType nil cons cons opType constTerm 65 remove appTerm 1167 def "Number.Natural.min" const 76 ref constTerm 1168 def 416 ref 1165 ref appTerm appTerm 416 ref 1166 ref appTerm appTerm appTerm appTerm appTerm 1169 def absTerm 1170 def absTerm 1171 def defineConst 1172 def pop 76 ref constTerm 1173 def 544 ref appTerm 18 ref appTerm appTerm 401 ref 1164 ref 438 ref 60 remove 457 ref 544 ref appTerm 458 ref appTerm 1174 def appTerm 459 ref appTerm absTerm appTerm 1167 ref 1168 remove 416 ref 544 ref appTerm 1175 def appTerm 421 ref appTerm appTerm appTerm appTerm appTerm absTerm appTerm absTerm 1176 def nil cons cons nil cons nil cons cons 45 ref subst 1161 remove nil 46 ref 52 ref 1162 ref 363 ref 1173 remove 1165 ref appTerm 1166 ref appTerm appTerm 1169 remove appTerm 1177 def absTerm 1178 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 5 ref 1178 remove nil cons cons nil cons nil cons cons 45 ref subst 1162 remove nil 46 ref 1177 remove nil cons cons nil cons nil cons cons 51 ref subst 1172 remove 1165 ref refl appThm 1171 remove 1165 remove appTerm betaConv trans 1166 ref refl appThm 1170 remove 1166 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 52 ref 1176 remove appTerm thm nil 5 ref 542 ref 52 ref 6 ref 363 ref "Number.Natural.Bits.or" "_28634" 1 ref var 1179 def "_28635" 1 remove var 1180 def 401 ref 1164 ref 438 ref 429 ref 457 ref 1179 ref varTerm 1181 def appTerm 458 ref appTerm appTerm 457 remove 1180 ref varTerm 1182 def appTerm 458 remove appTerm appTerm absTerm appTerm 1167 ref "Number.Natural.max" const 76 ref constTerm 1183 def 416 ref 1181 ref appTerm appTerm 416 remove 1182 ref appTerm appTerm appTerm appTerm appTerm 1184 def absTerm 1185 def absTerm 1186 def defineConst 1187 def pop 76 remove constTerm 1188 def 544 remove appTerm 18 remove appTerm appTerm 401 remove 1164 remove 438 remove 429 remove 1174 remove appTerm 459 remove appTerm absTerm appTerm 1167 remove 1183 remove 1175 remove appTerm 421 remove appTerm appTerm appTerm appTerm appTerm absTerm appTerm absTerm 1189 def nil cons cons nil cons nil cons cons 45 ref subst 1179 remove nil 46 ref 52 ref 1180 ref 363 ref 1188 remove 1181 ref appTerm 1182 ref appTerm appTerm 1184 remove appTerm 1190 def absTerm 1191 def appTerm nil cons cons nil cons nil cons cons 51 ref subst nil 5 remove 1191 remove nil cons cons nil cons nil cons cons 45 remove subst 1180 remove nil 46 remove 1190 remove nil cons cons nil cons nil cons cons 51 remove subst 1187 remove 1181 ref refl appThm 1186 remove 1181 remove appTerm betaConv trans 1182 ref refl appThm 1185 remove 1182 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 52 ref 1189 remove appTerm thm 1126 remove nil 52 ref 6 remove 52 remove 510 remove 506 ref 507 remove 363 remove 1137 remove appTerm 529 remove 530 remove 506 ref 531 remove 506 remove 532 remove 541 remove 361 remove 542 remove 546 remove 1136 remove 539 remove appTerm appTerm absTerm 403 remove appTerm absTerm 548 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 549 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm thm