path: "vendor/opentheory/data/theories/natural-prime-sieve-def/natural-prime-sieve-def.art"
6 version "Data.Bool.!" const 0 def "->" typeOp 1 def 1 ref "Number.Natural.natural" typeOp nil opType 2 def "bool" typeOp nil opType 3 def nil cons 4 def cons opType 5 def 4 ref cons opType 6 def constTerm 7 def refl 8 def "n" 2 ref var 9 def 8 ref "i" 2 ref var 10 def nil "t" 3 ref var 11 def "Number.Natural.Prime.Sieve.invariant.inv" "is_counters_sieve" 1 ref 2 ref 1 ref 2 ref 1 ref "Data.List.list" typeOp 12 def "Data.Pair.*" typeOp 13 def 2 ref 13 ref 2 ref 2 ref nil cons 14 def cons 15 def opType 16 def nil cons 17 def cons 18 def opType 19 def nil cons 20 def opType 21 def 4 ref cons opType 22 def nil cons cons opType nil cons cons opType 23 def var 24 def nil cons cons nil cons 24 ref "Data.Bool./\\" const 1 ref 3 ref 1 ref 3 ref 4 ref cons opType 25 def nil cons cons opType 26 def constTerm 27 def 7 ref 9 ref 7 ref 10 ref "=" const 28 def 26 ref constTerm 29 def 24 ref varTerm 30 def 9 ref varTerm 31 def appTerm 32 def 10 ref varTerm 33 def appTerm 34 def "Data.List.[]" const 35 def 21 ref constTerm 36 def appTerm appTerm "Data.Bool.T" const 3 ref constTerm 37 def appTerm absTerm appTerm absTerm appTerm appTerm 7 ref 9 ref 7 ref 10 ref 0 ref 1 ref 1 ref 19 ref 4 ref cons opType 38 def 4 ref cons opType 39 def constTerm 40 def "pkj" 19 ref var 41 def 0 ref 1 ref 22 ref 4 ref cons opType 42 def constTerm 43 def "ps" 21 ref var 44 def 29 ref 34 remove "Data.List.::" const 45 def 1 ref 19 ref 1 ref 21 ref 21 ref nil cons 46 def cons opType nil cons cons opType constTerm 47 def 41 ref varTerm 48 def appTerm 44 ref varTerm 49 def appTerm 50 def appTerm appTerm "select" const 51 def 1 ref 39 ref 38 ref nil cons 52 def cons opType constTerm 53 def "f" 38 ref var 54 def 7 ref "j" 2 ref var 55 def 7 ref "k" 2 ref var 56 def 7 ref "p" 2 ref var 57 def 29 ref 54 ref varTerm "Data.Pair.," const 58 def 1 ref 2 ref 1 ref 16 ref 20 ref cons opType nil cons cons opType constTerm 59 def 57 ref varTerm 60 def appTerm 61 def 58 ref 1 ref 2 ref 1 ref 18 remove opType nil cons cons opType constTerm 62 def 56 ref varTerm 63 def appTerm 55 ref varTerm 64 def appTerm 65 def appTerm 66 def appTerm appTerm 67 def 27 ref "Data.Bool.~" const 25 ref constTerm 68 def 28 ref 1 ref 2 ref 5 ref nil cons cons opType 69 def constTerm 70 def 60 ref appTerm "Number.Natural.zero" const 2 ref constTerm 71 def appTerm appTerm appTerm 72 def 27 ref 70 ref "Number.Natural.mod" const 1 ref 2 ref 1 ref 15 remove opType 73 def nil cons cons opType 74 def constTerm 75 def "Number.Natural.+" const 74 remove constTerm 76 def 63 ref appTerm 33 ref appTerm appTerm 60 ref appTerm 77 def appTerm 75 ref 31 ref appTerm 78 def 60 ref appTerm 79 def appTerm appTerm 80 def 32 remove 76 ref 33 ref appTerm 81 def 64 ref appTerm 82 def appTerm 49 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 48 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 83 def refl 84 def 28 ref 1 ref 23 ref 1 ref 23 ref 4 ref cons opType 85 def nil cons cons opType constTerm 86 def 30 ref appTerm 87 def 51 ref 1 ref 85 ref 23 ref nil cons 88 def cons opType constTerm 89 def 83 ref appTerm appTerm assume sym appThm 83 ref 30 ref appTerm betaConv 90 def trans "A" 88 remove cons nil cons 91 def nil nil cons 92 def cons nil 28 ref 1 ref 1 ref 1 ref "A" varType 93 def 4 ref cons opType 94 def 4 ref cons opType 95 def 1 ref 95 ref 4 ref cons opType 96 def nil cons cons opType constTerm 97 def "Data.Bool.?" const 98 def 95 ref constTerm 99 def appTerm 100 def "p" 94 ref var 101 def 101 ref varTerm 102 def 51 ref 1 ref 94 ref 93 ref nil cons 103 def cons opType constTerm 102 ref appTerm appTerm 104 def absTerm appTerm axiom 105 def subst 84 remove appThm "p" 85 ref var 106 def 106 remove varTerm 107 def 89 remove 107 remove appTerm appTerm absTerm 83 ref appTerm betaConv trans 98 ref 1 ref 1 ref 1 ref 21 ref 69 ref nil cons 108 def cons opType 109 def 4 ref cons opType 110 def 4 ref cons opType 111 def constTerm 112 def refl "fn" 109 ref var 113 def 27 ref 28 ref 1 ref 69 ref 1 ref 69 ref 4 ref cons opType nil cons cons opType constTerm 114 def 113 remove varTerm 115 def 36 ref appTerm appTerm 9 ref 10 ref 37 ref absTerm 116 def absTerm 117 def appTerm appTerm refl 40 ref refl 118 def "h" 19 ref var 119 def 43 ref refl 120 def "t" 21 ref var 121 def 114 ref 115 ref 47 ref 119 ref varTerm 122 def appTerm 121 ref varTerm 123 def appTerm 124 def appTerm appTerm refl 41 ref 44 ref "_29225" 69 ref var 125 def 9 ref 10 ref 53 ref 54 ref 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 67 ref 72 ref 80 ref 125 ref varTerm 31 ref appTerm 82 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 126 def 48 ref appTerm absTerm absTerm absTerm absTerm absTerm 127 def 122 ref appTerm betaConv 123 ref refl 128 def appThm 44 ref 125 remove 9 ref 10 ref 126 remove 122 ref appTerm absTerm absTerm absTerm 129 def absTerm 123 ref appTerm betaConv trans 115 remove 123 ref appTerm 130 def refl appThm 129 remove 130 remove appTerm betaConv trans appThm absThm appThm absThm appThm appThm absThm appThm nil "f" 1 ref 19 ref 1 ref 21 ref 1 ref 69 ref 108 ref cons opType nil cons cons opType nil cons cons opType var 127 remove nil cons cons "b" 69 remove var 117 ref nil cons cons nil cons cons nil cons cons "A" 20 remove cons 131 def "B" 108 remove cons nil cons cons 92 ref cons "f" 1 ref 93 ref 1 ref 12 ref 103 ref opType 132 def 1 ref "B" varType 133 def 133 ref nil cons 134 def cons opType nil cons 135 def cons opType nil cons cons opType 136 def var 137 def 98 ref 1 ref 1 ref 1 ref 132 ref 134 ref cons opType 138 def 4 ref cons opType 4 ref cons opType constTerm "fn" 138 remove var 139 def 27 ref 28 ref 1 ref 133 ref 1 ref 133 ref 4 ref cons opType 140 def nil cons cons opType constTerm 141 def 139 remove varTerm 142 def 35 ref 132 ref constTerm 143 def appTerm appTerm "b" 133 ref var 144 def varTerm 145 def appTerm appTerm 0 ref 95 ref constTerm 146 def "h" 93 ref var 147 def 0 ref 1 ref 1 ref 132 ref 4 ref cons opType 4 ref cons opType constTerm "t" 132 ref var 148 def 141 ref 142 ref 45 remove 1 ref 93 ref 1 ref 132 ref 132 ref nil cons cons opType nil cons cons opType constTerm 147 remove varTerm 149 def appTerm 148 remove varTerm 150 def appTerm appTerm appTerm 137 remove varTerm 151 def 149 remove appTerm 150 ref appTerm 142 remove 150 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm 152 def 151 ref appTerm 153 def betaConv 144 ref 0 ref 1 ref 1 ref 136 ref 4 ref cons opType 154 def 4 ref cons opType constTerm 152 ref appTerm 155 def absTerm 156 def 145 ref appTerm 157 def betaConv nil 0 ref 1 ref 140 ref 4 ref cons opType 158 def constTerm 159 def 156 ref appTerm 160 def axiom nil "p" 3 ref var 161 def 160 remove nil cons cons "q" 3 ref var 162 def 157 remove nil cons cons nil cons cons nil cons cons 29 ref "Data.Bool.==>" const 26 ref constTerm 163 def 161 ref varTerm 164 def appTerm 165 def 162 ref varTerm 166 def appTerm 167 def appTerm 168 def refl 161 ref 162 ref 29 ref 27 ref 164 ref appTerm 169 def 166 ref appTerm 170 def appTerm 171 def 164 ref appTerm absTerm 172 def absTerm 173 def 164 ref appTerm betaConv 166 ref refl 174 def appThm 172 remove 166 ref appTerm betaConv trans appThm nil 28 ref 1 ref 26 ref 1 ref 26 ref 4 ref cons opType 175 def nil cons cons opType constTerm 176 def 163 ref appTerm 173 remove appTerm axiom 164 ref refl 177 def appThm 174 ref appThm eqMp 178 def sym 179 def 171 remove refl 162 ref 28 ref 1 ref 175 ref 1 ref 175 remove 4 ref cons opType nil cons cons opType constTerm 180 def "f" 26 ref var 181 def 181 ref varTerm 182 def 164 ref appTerm 166 ref appTerm absTerm 183 def appTerm 181 ref 182 ref 37 ref appTerm 37 ref appTerm absTerm 184 def appTerm absTerm 185 def 166 ref appTerm betaConv appThm 28 ref 1 ref 25 ref 1 ref 25 ref 4 ref cons opType 186 def nil cons cons opType constTerm 187 def 169 remove appTerm refl 161 ref 185 remove absTerm 188 def 164 ref appTerm betaConv appThm nil 176 ref 27 ref appTerm 188 ref appTerm axiom 189 def 177 remove appThm eqMp 174 ref appThm eqMp 190 def sym 181 ref 182 ref refl nil 11 ref 164 ref nil cons 191 def cons nil cons nil cons cons 29 ref 11 ref varTerm 192 def appTerm 193 def 37 ref appTerm 194 def assume sym nil 37 ref axiom 195 def eqMp 192 ref assume 195 ref deductAntisym deductAntisym 196 def subst 164 ref assume 197 def eqMp appThm nil 11 ref 166 ref nil cons 198 def cons nil cons nil cons cons 196 ref subst 166 ref assume 199 def eqMp appThm absThm eqMp 200 def nil "P" 3 ref var 201 def 191 ref cons "Q" 3 ref var 202 def 198 ref cons nil cons 203 def cons nil cons cons 29 ref refl 204 def 181 ref 182 remove 201 ref varTerm 205 def appTerm 206 def 202 ref varTerm 207 def appTerm absTerm 208 def 161 ref 162 ref 164 ref absTerm absTerm 209 def appTerm betaConv 209 ref 205 ref appTerm betaConv 207 ref refl 210 def appThm 162 ref 205 ref absTerm 207 ref appTerm betaConv trans trans appThm 184 ref 209 ref appTerm betaConv 209 ref 37 ref appTerm betaConv 37 ref refl 211 def appThm 162 ref 37 ref absTerm 37 ref appTerm betaConv trans trans appThm 29 ref 27 ref 205 ref appTerm 212 def 207 ref appTerm 213 def appTerm refl 162 ref 180 remove 181 remove 206 remove 166 ref appTerm absTerm appTerm 184 ref appTerm absTerm 207 ref appTerm betaConv appThm 187 ref 212 remove appTerm refl 188 remove 205 ref appTerm betaConv appThm 189 remove 205 ref refl 214 def appThm eqMp 210 ref appThm eqMp 213 remove assume eqMp 215 def 209 remove refl appThm eqMp sym 195 ref eqMp 216 def subst 217 def deductAntisym eqMp 178 remove 167 ref assume eqMp sym 197 ref eqMp 204 ref 183 remove 161 ref 162 ref 166 ref absTerm 218 def absTerm 219 def appTerm betaConv 219 ref 164 ref appTerm betaConv 174 remove appThm 218 ref 166 ref appTerm betaConv trans trans appThm 184 remove 219 ref appTerm betaConv 219 ref 37 ref appTerm betaConv 211 ref appThm 218 ref 37 ref appTerm betaConv trans trans 220 def appThm 190 remove 170 remove assume eqMp 219 ref refl 221 def appThm eqMp sym 195 ref eqMp 222 def proveHyp 223 def deductAntisym 224 def subst proveHyp "A" 134 ref cons nil cons 225 def "P" 140 remove var 226 def 156 remove nil cons cons "x" 133 ref var 145 ref nil cons cons nil cons 227 def cons nil cons cons nil 161 ref 146 ref "P" 94 ref var 228 def varTerm 229 def appTerm 230 def nil cons 231 def cons 162 ref 229 ref "x" 93 ref var 232 def varTerm 233 def appTerm 234 def nil cons 235 def cons nil cons cons nil cons cons 236 def 179 ref subst 236 remove 222 remove 200 remove deductAntisym 237 def subst 29 ref 234 ref appTerm refl 232 ref 37 ref absTerm 238 def 233 ref appTerm betaConv appThm 101 ref 28 ref 1 ref 94 ref 95 ref nil cons cons opType constTerm 102 ref appTerm 238 remove appTerm absTerm 239 def 229 ref appTerm betaConv 240 def nil 97 remove 146 ref appTerm 239 remove appTerm axiom 229 ref refl 241 def appThm 242 def 230 ref assume eqMp eqMp 233 ref refl 243 def appThm eqMp sym 195 ref eqMp eqMp nil 201 ref 231 remove cons 202 ref 235 ref cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp 244 def subst eqMp eqMp nil 161 ref 155 remove nil cons cons 162 ref 153 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp "A" 136 ref nil cons cons nil cons "P" 154 remove var 152 remove nil cons cons "x" 136 remove var 151 remove nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp 245 def subst subst eqMp nil 161 ref 112 ref "_29224" 109 ref var 246 def 27 ref 114 ref 246 ref varTerm 247 def 36 ref appTerm 248 def appTerm 117 ref appTerm 249 def appTerm 250 def 40 ref 41 ref 43 ref 44 ref 114 ref 247 ref 50 ref appTerm 251 def appTerm 9 ref 10 ref 53 ref 54 ref 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 67 ref 72 ref 80 ref 247 ref 49 ref appTerm 31 ref appTerm 82 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 48 ref appTerm 252 def absTerm 253 def absTerm 254 def appTerm absTerm 255 def appTerm 256 def absTerm 257 def appTerm 258 def appTerm 259 def absTerm 260 def appTerm 261 def nil cons cons 162 ref 112 remove 246 ref 27 ref 7 ref 9 ref 7 ref 10 ref 29 ref 248 remove 31 ref appTerm 262 def 33 ref appTerm appTerm 263 def 37 ref appTerm 264 def absTerm 265 def appTerm 266 def absTerm 267 def appTerm 268 def appTerm 7 ref 9 ref 7 ref 10 ref 40 ref 41 ref 43 ref 44 ref 29 ref 251 remove 31 ref appTerm 269 def 33 ref appTerm appTerm 270 def 252 remove appTerm 271 def absTerm 272 def appTerm 273 def absTerm 274 def appTerm 275 def absTerm 276 def appTerm 277 def absTerm 278 def appTerm 279 def appTerm 280 def absTerm 281 def appTerm 282 def nil cons 283 def cons nil cons 284 def cons nil cons cons 224 ref subst nil "P" 110 remove var 285 def 246 ref 163 ref 260 ref 247 ref appTerm 286 def appTerm 282 ref appTerm 287 def absTerm nil cons cons nil cons nil cons cons "A" 109 ref nil cons cons nil cons 288 def 92 ref cons 29 ref 230 remove appTerm refl 240 remove appThm 242 remove eqMp sym 289 def subst 290 def subst 246 ref nil 11 ref 287 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 286 remove nil cons 291 def cons 284 ref cons nil cons cons 292 def 179 ref subst 292 remove 237 ref subst 246 ref 250 remove 40 ref 119 ref 43 ref 121 ref 114 ref 247 ref 124 ref appTerm appTerm 9 ref 10 ref 53 ref 54 ref 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 67 ref 72 ref 80 ref 247 ref 123 ref appTerm 31 ref appTerm 82 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 122 ref appTerm absTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 247 ref appTerm 293 def betaConv 293 remove assume eqMp nil 161 ref 259 remove nil cons 294 def cons 284 remove cons nil cons cons 295 def 224 ref subst proveHyp 295 ref 179 ref subst 295 remove 237 ref subst 281 ref 247 ref appTerm 296 def betaConv 297 def sym nil 201 ref 249 ref nil cons cons 202 ref 258 remove nil cons 298 def cons nil cons cons nil cons cons 299 def 216 ref subst nil "P" 5 ref var 300 def 267 remove nil cons cons nil cons nil cons cons "A" 14 ref cons 301 def nil cons 302 def 92 ref cons 303 def 289 ref subst 304 def subst 9 ref nil 11 ref 266 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 265 remove nil cons cons nil cons nil cons cons 304 ref subst 10 ref nil 11 ref 264 remove nil cons cons nil cons nil cons cons 196 ref subst 263 remove refl 116 remove 33 ref appTerm betaConv appThm 28 ref 1 ref 5 remove 6 remove nil cons cons opType constTerm 305 def 262 remove appTerm refl 117 remove 31 ref appTerm betaConv appThm 249 remove assume 31 ref refl 306 def appThm eqMp 33 ref refl 307 def appThm eqMp eqMp absThm eqMp eqMp absThm eqMp proveHyp nil 161 ref 268 remove nil cons cons 162 ref 279 remove nil cons cons nil cons cons nil cons cons 237 ref subst proveHyp 299 remove 204 ref 208 remove 219 ref appTerm betaConv 219 remove 205 ref appTerm betaConv 210 ref appThm 218 remove 207 ref appTerm betaConv trans trans appThm 220 remove appThm 215 remove 221 remove appThm eqMp sym 195 ref eqMp 308 def subst nil 300 ref 278 remove nil cons cons nil cons nil cons cons 304 ref subst 9 ref nil 11 ref 277 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 276 remove nil cons cons nil cons nil cons cons 304 ref subst 10 ref nil 11 ref 275 remove nil cons cons nil cons nil cons cons 196 ref subst nil "P" 38 ref var 309 def 274 remove nil cons cons nil cons nil cons cons 131 ref nil cons 310 def 92 ref cons 289 ref subst 311 def subst 41 ref nil 11 ref 273 remove nil cons cons nil cons nil cons cons 196 ref subst nil "P" 22 ref var 312 def 272 remove nil cons cons nil cons nil cons cons "A" 46 ref cons nil cons 313 def 92 ref cons 289 ref subst 314 def subst 44 ref nil 11 ref 271 remove nil cons cons nil cons nil cons cons 196 ref subst 270 remove refl 253 remove 33 ref appTerm betaConv appThm 305 ref 269 remove appTerm refl 254 remove 31 ref appTerm betaConv appThm 255 ref 49 ref appTerm 315 def betaConv 257 ref 48 ref appTerm 316 def betaConv nil 161 ref 298 remove cons 162 ref 316 remove nil cons cons nil cons cons nil cons cons 224 ref subst 310 ref 309 ref 257 remove nil cons cons "x" 19 ref var 48 ref nil cons cons nil cons 317 def cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 256 remove nil cons cons 162 ref 315 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 313 ref 312 ref 255 remove nil cons cons "x" 21 ref var 49 ref nil cons 318 def cons nil cons 319 def cons nil cons cons 244 ref subst eqMp eqMp 306 ref appThm eqMp 307 ref appThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp proveHyp eqMp eqMp 288 ref 285 ref 281 ref nil cons cons 320 def "x" 109 remove var 321 def 247 ref nil cons cons nil cons cons nil cons cons 29 ref 99 ref 229 ref appTerm 322 def appTerm 323 def refl 101 ref 0 ref 186 ref constTerm 324 def 162 ref 163 ref 146 ref 232 ref 163 ref 102 ref 233 ref appTerm 325 def appTerm 326 def 166 ref appTerm absTerm appTerm appTerm 166 ref appTerm absTerm appTerm absTerm 327 def 229 remove appTerm betaConv appThm nil 100 remove 327 remove appTerm axiom 241 remove appThm eqMp 328 def sym nil "P" 25 remove var 329 def 202 ref 163 ref 146 ref 232 ref 163 ref 234 ref appTerm 330 def 207 ref appTerm 331 def absTerm 332 def appTerm 333 def appTerm 334 def 207 ref appTerm 335 def absTerm nil cons cons nil cons nil cons cons "A" 4 ref cons 336 def nil cons 337 def 92 ref cons 338 def 289 ref subst 339 def subst 202 ref nil 11 ref 335 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 333 ref nil cons 340 def cons 341 def 162 ref 207 ref nil cons 342 def cons nil cons 343 def cons nil cons cons 344 def 179 ref subst 344 ref 237 ref subst nil 161 ref 235 ref cons 343 ref cons nil cons cons 345 def 224 ref subst 346 def 332 ref 233 ref appTerm 347 def betaConv nil 341 ref 162 ref 347 remove nil cons cons nil cons cons nil cons cons 224 ref subst "A" 103 ref cons 348 def nil cons 349 def 228 ref 332 remove nil cons cons 350 def 232 ref 233 ref nil cons cons nil cons 351 def cons nil cons cons 244 ref subst eqMp eqMp 352 def eqMp eqMp nil 201 ref 340 ref cons 353 def 202 ref 342 ref cons nil cons 354 def cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 355 def subst proveHyp eqMp nil 201 ref 294 remove cons 202 ref 283 ref cons nil cons 356 def cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp nil 201 ref 291 remove cons 356 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp nil 161 ref 0 ref 111 remove constTerm 357 def 321 ref 163 ref 260 ref 321 ref varTerm 358 def appTerm appTerm 282 ref appTerm absTerm appTerm nil cons cons 162 ref 163 ref 261 remove appTerm 282 ref appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 288 ref 285 ref 260 remove nil cons cons 356 remove cons nil cons cons nil 341 ref 162 ref 163 ref 322 ref appTerm 359 def 207 ref appTerm nil cons 360 def cons nil cons cons nil cons cons 361 def 179 ref subst 361 remove 237 ref subst nil 161 ref 322 remove nil cons 362 def cons 363 def 343 ref cons nil cons cons 364 def 179 ref subst 364 remove 237 ref subst 344 remove 224 ref subst 162 ref 163 ref 146 ref 232 ref 330 remove 166 ref appTerm absTerm appTerm appTerm 166 ref appTerm absTerm 365 def 207 ref appTerm 366 def betaConv nil 363 remove 162 ref 324 ref 365 ref appTerm 367 def nil cons 368 def cons nil cons cons nil cons cons 369 def 224 ref subst 328 remove nil 161 ref 323 remove 367 ref appTerm nil cons cons 162 ref 359 remove 367 remove appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 369 remove nil 161 ref 29 ref 164 ref appTerm 370 def 166 ref appTerm 371 def nil cons 372 def cons 373 def 162 ref 167 ref nil cons 374 def cons nil cons 375 def cons nil cons cons 376 def 179 ref subst 376 remove 237 ref subst 179 ref 237 ref 371 remove assume 377 def 197 remove eqMp eqMp 217 ref deductAntisym eqMp 378 def eqMp nil 201 ref 372 remove cons 379 def 202 ref 374 ref cons nil cons 380 def cons nil cons cons 216 ref subst deductAntisym eqMp 381 def subst eqMp eqMp nil 161 ref 368 remove cons 162 ref 366 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 365 remove nil cons cons "x" 3 ref var 382 def 342 remove cons nil cons cons nil cons cons 244 ref subst eqMp eqMp eqMp eqMp nil 201 ref 362 remove cons 354 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp nil 353 ref 202 ref 360 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp 383 def subst eqMp eqMp proveHyp nil 161 ref 283 remove cons 162 ref 98 ref 1 ref 85 ref 4 ref cons opType constTerm 83 ref appTerm 384 def nil cons 385 def cons nil cons 386 def cons nil cons cons 224 ref subst nil 285 remove 246 ref 163 ref 296 ref appTerm 384 ref appTerm 387 def absTerm nil cons cons nil cons nil cons cons 290 remove subst 246 remove nil 11 ref 387 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 296 ref nil cons 388 def cons 386 ref cons nil cons cons 389 def 179 ref subst 389 remove 237 ref subst 297 remove 296 remove assume eqMp nil 161 ref 280 ref nil cons 390 def cons 386 ref cons nil cons cons 391 def 224 ref subst proveHyp 391 ref 179 ref subst 391 remove 237 ref subst "_29221" 2 ref var 392 def "_29222" 2 ref var 393 def "_29223" 21 ref var 394 def 247 remove 394 ref varTerm appTerm 395 def 392 remove varTerm appTerm 393 ref varTerm 396 def appTerm absTerm absTerm absTerm 397 def refl nil 161 ref 86 remove 397 ref appTerm 397 ref appTerm nil cons cons 386 ref cons nil cons cons 224 ref subst proveHyp nil 24 remove 397 ref nil cons cons nil cons nil cons cons nil 161 ref 87 remove 397 ref appTerm 398 def nil cons 399 def cons 386 remove cons nil cons cons 400 def 179 ref subst 400 remove 237 ref subst 90 remove sym 27 ref refl 401 def 8 ref 9 ref 8 ref 10 ref 204 ref 398 remove assume 306 ref appThm 397 remove 31 ref appTerm betaConv trans 402 def 307 ref appThm 393 remove 394 ref 395 remove 31 ref appTerm 403 def 396 remove appTerm absTerm absTerm 404 def 33 ref appTerm betaConv trans 405 def 36 ref refl 406 def appThm 394 ref 403 ref 33 ref appTerm absTerm 407 def 36 ref appTerm betaConv trans appThm 211 remove appThm absThm appThm absThm appThm appThm 8 ref 9 ref 8 ref 10 ref 118 ref 41 ref 120 ref 44 ref 204 ref 405 remove 50 ref refl 408 def appThm 407 remove 50 ref appTerm betaConv trans appThm 53 ref refl 54 ref 8 ref 55 ref 8 ref 56 ref 8 ref 57 ref 67 ref refl 72 ref refl 80 ref refl 402 remove 82 ref refl appThm 404 remove 82 ref appTerm betaConv trans 49 ref refl 409 def appThm 394 remove 403 remove 82 ref appTerm absTerm 49 ref appTerm betaConv trans appThm appThm appThm absThm appThm absThm appThm absThm appThm absThm appThm 48 ref refl 410 def appThm appThm absThm appThm absThm appThm absThm appThm absThm appThm appThm sym 280 remove assume eqMp eqMp 91 remove "P" 85 remove var 83 remove nil cons cons "x" 23 ref var 30 remove nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp eqMp nil 201 ref 399 remove cons 202 ref 385 remove cons nil cons 411 def cons nil cons cons 216 ref subst deductAntisym eqMp subst eqMp eqMp nil 201 ref 390 remove cons 411 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp nil 201 ref 388 remove cons 411 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp nil 161 ref 357 remove 321 remove 163 ref 281 remove 358 remove appTerm appTerm 384 ref appTerm absTerm appTerm nil cons cons 162 ref 163 ref 282 remove appTerm 384 remove appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 288 remove 320 remove 411 remove cons nil cons cons 383 ref subst eqMp eqMp proveHyp eqMp eqMp defineConstList 412 def pop hdTl pop 23 remove constTerm 413 def 31 ref appTerm 414 def 33 ref appTerm 415 def 36 ref appTerm 416 def nil cons cons nil cons nil cons cons 417 def 11 ref 29 ref 194 ref appTerm 192 ref appTerm absTerm 418 def 192 ref appTerm 419 def betaConv nil 324 ref 418 ref appTerm 420 def axiom nil 161 ref 420 remove nil cons cons 162 ref 419 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 418 remove nil cons cons 382 ref 192 ref nil cons cons nil cons 421 def cons nil cons cons 244 ref subst eqMp eqMp subst absThm appThm absThm appThm 412 ref nil 201 ref 7 ref 9 ref 7 ref 10 ref 29 ref 416 ref appTerm 37 ref appTerm absTerm appTerm absTerm appTerm nil cons cons 202 ref 7 ref 9 ref 7 ref 10 ref 40 ref 41 ref 43 ref 44 ref 29 ref 415 ref 50 ref appTerm appTerm 53 ref 54 remove 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 67 remove 72 ref 80 ref 414 ref 82 remove appTerm 49 ref appTerm appTerm appTerm 422 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 48 ref appTerm appTerm absTerm 423 def appTerm 424 def absTerm 425 def appTerm 426 def absTerm 427 def appTerm 428 def absTerm 429 def appTerm nil cons 430 def cons nil cons cons nil cons cons 431 def 216 ref subst proveHyp eqMp 432 def nil 7 ref 9 ref 7 ref 10 ref 416 remove absTerm 433 def appTerm 434 def absTerm 435 def appTerm 436 def thm nil 300 ref 9 ref 7 ref 10 ref 7 ref 57 ref 7 ref 56 ref 7 ref 55 ref 43 ref 44 ref 29 ref 415 remove 47 ref 66 ref appTerm 49 ref appTerm 437 def appTerm appTerm 422 ref appTerm 438 def absTerm 439 def appTerm 440 def absTerm 441 def appTerm 442 def absTerm 443 def appTerm 444 def absTerm 445 def appTerm 446 def absTerm 447 def appTerm 448 def absTerm 449 def nil cons cons nil cons nil cons cons 304 ref subst 9 ref nil 11 ref 448 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 447 remove nil cons cons nil cons nil cons cons 304 ref subst 10 ref nil 11 ref 446 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 445 remove nil cons cons nil cons nil cons cons 304 ref subst 57 ref nil 11 ref 444 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 443 remove nil cons cons nil cons nil cons cons 304 ref subst 56 ref nil 11 ref 442 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 441 remove nil cons cons nil cons nil cons cons 304 ref subst 55 ref nil 11 ref 440 remove nil cons cons nil cons nil cons cons 196 ref subst nil 312 ref 439 remove nil cons cons nil cons nil cons cons 314 ref subst 44 ref nil 11 ref 438 remove nil cons cons nil cons nil cons cons 196 ref subst 204 ref nil 41 ref 66 ref nil cons cons nil cons nil cons cons 450 def 423 ref 49 ref appTerm 451 def betaConv 425 ref 48 ref appTerm 452 def betaConv 427 ref 33 ref appTerm 453 def betaConv 429 ref 31 ref appTerm 454 def betaConv 412 remove 431 remove 308 ref subst proveHyp nil 161 ref 430 remove cons 162 ref 454 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 429 remove nil cons cons "x" 2 ref var 455 def 31 ref nil cons 456 def cons nil cons 457 def cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 428 remove nil cons cons 162 ref 453 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 427 remove nil cons cons 455 ref 33 ref nil cons cons nil cons 458 def cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 426 remove nil cons cons 162 ref 452 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 310 ref 309 ref 425 remove nil cons cons 317 ref cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 424 remove nil cons cons 162 ref 451 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 313 ref 312 ref 423 remove nil cons cons 319 ref cons nil cons cons 244 ref subst eqMp eqMp subst appThm 422 ref refl appThm sym 57 ref 29 ref 53 remove "_29246" 38 ref var 459 def 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 29 ref 459 remove varTerm 66 ref appTerm appTerm 422 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 460 def appTerm 461 def 66 ref appTerm appTerm 422 ref appTerm absTerm 462 def 60 ref appTerm 463 def betaConv 56 ref 7 ref 462 ref appTerm 464 def absTerm 465 def 63 ref appTerm 466 def betaConv 55 ref 7 ref 465 ref appTerm 467 def absTerm 468 def 64 ref appTerm 469 def betaConv 460 ref 461 remove appTerm 470 def betaConv 460 ref "_29244" 19 ref var 471 def 27 ref 68 ref 70 ref 51 ref 1 ref 1 ref 1 ref 19 ref 14 ref cons opType 472 def 4 ref cons opType 472 ref nil cons cons opType constTerm "fn" 472 ref var 473 def 7 ref "a" 2 ref var 474 def 0 ref 1 ref 1 ref 16 ref 4 ref cons opType 475 def 4 ref cons opType constTerm 476 def "b" 16 ref var 477 def 70 ref 473 remove varTerm 59 ref 474 ref varTerm 478 def appTerm 477 ref varTerm 479 def appTerm 480 def appTerm appTerm 478 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 481 def 471 remove varTerm 482 def appTerm 483 def appTerm 71 ref appTerm appTerm appTerm 27 ref 70 ref 75 ref 76 ref 51 ref 1 ref 1 ref 1 ref 16 ref 14 ref cons opType 484 def 4 ref cons opType 484 ref nil cons cons opType constTerm 485 def "fn" 484 remove var 486 def 7 ref 474 ref 7 ref "b" 2 ref var 487 def 70 ref 486 ref varTerm 62 ref 478 ref appTerm 487 ref varTerm 488 def appTerm appTerm appTerm 489 def 478 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 490 def 51 ref 1 ref 1 ref 1 ref 19 ref 17 ref cons opType 491 def 4 ref cons opType 491 ref nil cons cons opType constTerm "fn" 491 remove var 492 def 7 ref 474 ref 476 remove 477 ref 28 ref 1 ref 16 ref 475 remove nil cons cons opType constTerm 492 remove varTerm 480 remove appTerm appTerm 479 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 493 def 482 remove appTerm 494 def appTerm appTerm 33 ref appTerm appTerm 483 ref appTerm appTerm 78 ref 483 remove appTerm appTerm appTerm 414 ref 81 ref 485 remove 486 remove 7 ref 474 ref 7 ref 487 ref 489 remove 488 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 495 def 494 remove appTerm appTerm appTerm 49 ref appTerm appTerm appTerm absTerm 496 def appTerm betaConv sym nil 300 ref 55 ref 7 ref 56 ref 7 ref 57 ref 29 ref 496 ref 66 ref appTerm 497 def appTerm 422 remove appTerm 498 def absTerm 499 def appTerm 500 def absTerm 501 def appTerm 502 def absTerm nil cons cons nil cons nil cons cons 304 ref subst 55 ref nil 11 ref 502 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 501 remove nil cons cons nil cons nil cons cons 304 ref subst 56 ref nil 11 ref 500 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 499 remove nil cons cons nil cons nil cons cons 304 ref subst 57 ref nil 11 ref 498 remove nil cons cons nil cons nil cons cons 196 ref subst 497 remove betaConv 29 ref "_29240" 2 ref var 503 def 72 ref 80 remove 414 ref 81 ref 503 ref varTerm appTerm appTerm 49 ref appTerm 504 def appTerm appTerm absTerm 64 ref appTerm 505 def appTerm refl 503 ref 27 ref 68 ref 70 ref 481 ref 66 ref appTerm 506 def appTerm 71 ref appTerm appTerm appTerm 507 def 27 ref 70 ref 75 ref 76 ref 490 ref 493 ref 66 ref appTerm 508 def appTerm 509 def appTerm 33 ref appTerm appTerm 506 ref appTerm 510 def appTerm 78 ref 506 ref appTerm 511 def appTerm appTerm 512 def 504 ref appTerm appTerm absTerm 513 def 495 ref 508 ref appTerm 514 def appTerm betaConv appThm 204 ref 505 remove betaConv appThm 507 ref 512 remove 414 ref 81 remove 514 ref appTerm appTerm 49 ref appTerm appTerm appTerm refl appThm trans 305 ref "_29239" 2 ref var 515 def 503 ref 72 remove 27 ref 70 ref 75 ref 76 ref 515 ref varTerm appTerm 33 ref appTerm appTerm 516 def 60 ref appTerm appTerm 79 remove appTerm appTerm 504 ref appTerm appTerm absTerm absTerm 63 ref appTerm 517 def appTerm refl 515 ref 503 ref 507 remove 27 ref 70 ref 516 ref 506 ref appTerm appTerm 511 remove appTerm appTerm 504 ref appTerm appTerm absTerm absTerm 518 def 509 ref appTerm betaConv appThm 305 remove refl 517 remove betaConv appThm 513 remove refl appThm trans 114 ref "_29238" 2 ref var 519 def 515 remove 503 remove 27 ref 68 ref 70 ref 519 remove varTerm 520 def appTerm 71 ref appTerm appTerm appTerm 27 ref 70 ref 516 remove 520 ref appTerm appTerm 78 remove 520 remove appTerm appTerm appTerm 504 remove appTerm appTerm absTerm absTerm absTerm 521 def 60 ref appTerm 522 def appTerm refl 521 ref 506 ref appTerm betaConv appThm 114 remove refl 522 remove betaConv appThm 518 remove refl appThm trans 521 remove refl nil 477 remove 65 ref nil cons cons 474 ref 60 ref nil cons 523 def cons nil cons cons nil cons cons 524 def 301 ref "B" 17 remove cons nil cons cons 92 ref cons 525 def 144 ref 28 ref 1 ref 93 ref 94 ref nil cons 526 def cons opType constTerm 527 def 51 ref 1 ref 1 ref 1 ref 13 ref 93 ref 134 ref cons 528 def opType 529 def 103 ref cons opType 530 def 4 ref cons opType 531 def 530 ref nil cons 532 def cons opType constTerm "fn" 530 ref var 533 def 146 ref "a" 93 ref var 534 def 159 ref 144 ref 527 ref 533 ref varTerm 58 ref 1 ref 93 ref 1 ref 133 ref 529 ref nil cons cons opType nil cons cons opType constTerm 534 ref varTerm 535 def appTerm 145 ref appTerm 536 def appTerm appTerm 537 def 535 ref appTerm absTerm appTerm absTerm appTerm absTerm 538 def appTerm 539 def 536 ref appTerm appTerm 535 ref appTerm absTerm 540 def 145 ref appTerm 541 def betaConv 534 ref 159 ref 540 ref appTerm 542 def absTerm 543 def 535 ref appTerm 544 def betaConv 538 ref 539 remove appTerm 545 def betaConv 98 ref 1 ref 531 ref 4 ref cons opType constTerm 546 def refl 533 remove 146 ref refl 547 def 534 ref 159 ref refl 548 def 144 ref 537 remove refl 534 ref 144 ref 535 ref absTerm 549 def absTerm 550 def 535 ref appTerm betaConv 145 ref refl 551 def appThm 549 remove 145 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 103 ref cons nil cons "_1343" 1 ref 93 ref 1 ref 133 ref 103 ref cons opType nil cons cons opType var 550 remove nil cons cons nil cons nil cons cons nil "f" 1 ref 93 ref 1 ref 133 ref "C" varType 552 def nil cons 553 def cons opType nil cons cons opType 554 def var 555 def 534 ref 144 ref "_1343" 554 ref var varTerm 535 ref appTerm 145 ref appTerm 556 def absTerm 557 def absTerm 558 def nil cons cons nil cons nil cons cons 555 ref 98 ref 1 ref 1 ref 1 ref 529 ref 553 remove cons opType 559 def 4 ref cons opType 560 def 4 ref cons opType 561 def constTerm 562 def "fn" 559 ref var 563 def 146 ref 534 ref 159 ref 144 ref 28 ref 1 ref 552 ref 1 ref 552 remove 4 ref cons opType nil cons cons opType constTerm 563 ref varTerm 564 def 536 ref appTerm appTerm 565 def 555 remove varTerm 566 def 535 ref appTerm 145 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 567 def 566 ref appTerm 568 def betaConv nil 0 ref 1 ref 1 ref 554 ref 4 ref cons opType 569 def 4 ref cons opType constTerm 567 ref appTerm 570 def axiom nil 161 ref 570 remove nil cons cons 162 ref 568 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp "A" 554 ref nil cons cons nil cons "P" 569 remove var 567 remove nil cons cons "x" 554 remove var 566 remove nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp subst nil 161 ref 562 ref 563 ref 146 ref 534 ref 159 ref 144 ref 565 ref 558 remove 535 ref appTerm 571 def 145 ref appTerm appTerm absTerm appTerm absTerm appTerm 572 def absTerm 573 def appTerm 574 def nil cons cons 162 ref 562 remove 563 ref 146 ref 534 ref 159 ref 144 ref 565 ref 556 remove appTerm absTerm appTerm absTerm appTerm absTerm 575 def appTerm 576 def nil cons 577 def cons nil cons 578 def cons nil cons cons 224 ref subst nil "P" 560 remove var 579 def 563 ref 163 ref 573 ref 564 ref appTerm 580 def appTerm 576 ref appTerm 581 def absTerm nil cons cons nil cons nil cons cons "A" 559 ref nil cons cons nil cons 582 def 92 ref cons 289 ref subst subst 563 remove nil 11 ref 581 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 580 ref nil cons 583 def cons 578 ref cons nil cons cons 584 def 179 ref subst 584 remove 237 ref subst 580 ref betaConv 580 remove assume eqMp nil 161 ref 572 ref nil cons 585 def cons 578 remove cons nil cons cons 586 def 224 ref subst proveHyp 586 ref 179 ref subst 586 remove 237 ref subst 575 ref 564 ref appTerm betaConv sym 547 ref 534 ref 548 ref 144 ref 565 remove refl 571 remove betaConv 551 ref appThm 557 remove 145 ref appTerm betaConv trans appThm absThm appThm absThm appThm 572 remove assume eqMp eqMp 582 ref 579 ref 575 remove nil cons cons "x" 559 remove var 587 def 564 remove nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp eqMp nil 201 ref 585 remove cons 202 ref 577 remove cons nil cons 588 def cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp nil 201 ref 583 remove cons 588 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp nil 161 ref 0 ref 561 remove constTerm 587 ref 163 ref 573 ref 587 remove varTerm appTerm appTerm 576 ref appTerm absTerm appTerm nil cons cons 162 ref 163 ref 574 remove appTerm 576 remove appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 582 remove 579 remove 573 remove nil cons cons 588 remove cons nil cons cons 383 ref subst eqMp eqMp proveHyp 589 def subst eqMp nil 161 ref 546 remove 538 ref appTerm nil cons cons 162 ref 545 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp "A" 532 remove cons nil cons "p" 531 remove var 538 remove nil cons cons nil cons nil cons cons nil 161 ref 99 ref 102 ref appTerm 590 def nil cons 591 def cons 592 def 162 ref 29 ref 104 ref appTerm 593 def 37 ref appTerm 594 def nil cons 595 def cons nil cons 596 def cons nil cons cons 597 def 179 ref subst 597 remove 237 ref subst 99 ref refl nil "t" 94 ref var 102 ref nil cons 598 def cons nil cons nil cons cons 348 remove "B" 4 ref cons nil cons cons 92 ref cons "t" 1 ref 528 remove opType 599 def var 600 def 28 ref 1 ref 599 ref 1 ref 599 ref 4 ref cons opType 601 def nil cons cons opType constTerm 232 ref 600 remove varTerm 602 def 233 ref appTerm absTerm appTerm 602 ref appTerm absTerm 603 def 602 ref appTerm 604 def betaConv nil 0 ref 1 ref 601 ref 4 ref cons opType 605 def constTerm 606 def 603 ref appTerm 607 def axiom nil 161 ref 607 remove nil cons cons 162 ref 604 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp "A" 599 ref nil cons cons nil cons 608 def "P" 601 remove var 609 def 603 remove nil cons cons "x" 599 ref var 610 def 602 remove nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp subst subst appThm nil 11 ref 591 ref cons nil cons nil cons cons 611 def 196 ref subst 590 ref assume eqMp trans sym 195 ref eqMp nil 161 ref 99 ref 232 ref 325 ref absTerm appTerm nil cons cons 596 ref cons nil cons cons 224 ref subst proveHyp nil 228 ref 598 ref cons 202 ref 595 remove cons nil cons 612 def cons nil cons cons nil 341 remove 162 ref 163 ref 99 ref 232 ref 234 ref absTerm 613 def appTerm 614 def appTerm 207 ref appTerm 615 def nil cons 616 def cons nil cons 617 def cons nil cons cons 618 def 378 remove nil 161 ref 374 ref cons 619 def 162 ref 163 ref 166 ref appTerm 620 def 164 ref appTerm nil cons 621 def cons nil cons 622 def cons nil cons cons 237 ref subst proveHyp 620 ref refl 377 remove appThm sym nil 161 ref 198 ref cons 623 def 162 ref 198 ref cons nil cons 624 def cons nil cons cons 625 def 179 ref subst 625 remove 237 ref subst 199 remove eqMp nil 201 ref 198 remove cons 203 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp 626 def eqMp nil 623 ref 162 ref 191 ref cons nil cons 627 def cons nil cons cons 224 ref subst nil 201 ref 374 remove cons 628 def 202 ref 621 remove cons nil cons 629 def cons nil cons cons 630 def 308 ref subst eqMp 224 ref 630 remove 216 ref subst eqMp deductAntisym deductAntisym 631 def subst 618 ref 179 ref subst 618 remove 237 ref subst nil 228 ref 232 ref 163 ref 613 ref 233 ref appTerm 632 def appTerm 207 ref appTerm 633 def absTerm 634 def nil cons cons nil cons nil cons cons 289 ref subst 232 ref nil 11 ref 633 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 632 ref nil cons 635 def cons 343 ref cons nil cons cons 636 def 179 ref subst 636 remove 237 ref subst 632 ref betaConv 637 def 632 remove assume eqMp 346 remove proveHyp 352 remove eqMp eqMp nil 201 ref 635 remove cons 354 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp nil 161 ref 146 ref 634 remove appTerm nil cons cons 617 remove cons nil cons cons 224 ref subst proveHyp 349 ref 228 ref 613 remove nil cons cons 638 def 354 ref cons nil cons cons 383 ref subst eqMp eqMp nil 353 remove 202 ref 616 ref cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp nil 161 ref 334 remove 615 ref appTerm nil cons cons 162 ref 163 ref 615 ref appTerm 333 remove appTerm nil cons cons nil cons cons nil cons cons 237 ref subst proveHyp nil 161 ref 616 ref cons 162 ref 340 ref cons nil cons cons nil cons cons 639 def 179 ref subst 639 remove 237 ref subst nil 350 remove nil cons nil cons cons 289 ref subst 232 ref nil 11 ref 331 remove nil cons cons nil cons nil cons cons 196 ref subst 345 ref 179 ref subst 345 remove 237 ref subst 637 remove sym 234 remove assume eqMp 349 ref 638 remove 351 ref cons nil cons cons 355 ref subst proveHyp nil 161 ref 614 remove nil cons cons 343 remove cons nil cons cons 224 ref subst 615 remove assume eqMp proveHyp eqMp nil 201 ref 235 remove cons 354 remove cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 201 ref 616 remove cons 202 ref 340 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp subst nil 228 ref 232 ref 326 ref 594 ref appTerm 640 def absTerm nil cons cons nil cons nil cons cons 289 ref subst 232 ref nil 11 ref 640 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 325 ref nil cons 641 def cons 642 def 596 remove cons nil cons cons 643 def 179 ref subst 643 remove 237 ref subst nil 11 ref 104 ref nil cons 644 def cons nil cons nil cons cons 196 ref subst nil 642 remove 162 ref 644 remove cons 645 def nil cons cons nil cons cons 224 ref subst 232 ref 326 remove 104 ref appTerm absTerm 646 def 233 ref appTerm 647 def betaConv 101 ref 146 ref 646 ref appTerm 648 def absTerm 649 def 102 remove appTerm 650 def betaConv nil 0 ref 96 remove constTerm 651 def 649 ref appTerm 652 def axiom nil 161 ref 652 remove nil cons cons 162 ref 650 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp "A" 526 remove cons nil cons "P" 95 remove var 649 remove nil cons cons "x" 94 remove var 598 remove cons nil cons cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 648 remove nil cons cons 162 ref 647 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 349 ref 228 ref 646 remove nil cons cons 351 remove cons nil cons cons 244 ref subst eqMp eqMp eqMp eqMp eqMp nil 201 ref 641 remove cons 612 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp eqMp eqMp nil 201 ref 591 ref cons 612 remove cons nil cons cons 216 ref subst deductAntisym eqMp nil 161 ref 163 ref 590 ref appTerm 653 def 594 remove appTerm nil cons cons 162 ref 29 ref 653 ref 104 remove appTerm appTerm 654 def 653 ref 37 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp nil "q'" 3 ref var 655 def 37 ref nil cons cons nil cons nil cons cons 590 ref refl nil 161 ref 29 ref 590 ref appTerm 656 def 590 remove appTerm nil cons cons 162 ref 163 ref 653 ref 593 remove 655 ref varTerm 657 def appTerm 658 def appTerm appTerm 654 ref 653 remove 657 ref appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp nil "p'" 3 ref var 659 def 591 remove cons nil cons nil cons cons 655 ref 163 ref 656 remove 659 ref varTerm 660 def appTerm appTerm 163 ref 163 ref 660 ref appTerm 661 def 658 remove appTerm appTerm 654 remove 661 ref 657 ref appTerm 662 def appTerm appTerm appTerm absTerm 663 def 657 ref appTerm 664 def betaConv 659 ref 324 ref 663 ref appTerm 665 def absTerm 666 def 660 ref appTerm 667 def betaConv nil 645 remove 592 remove nil cons cons nil cons cons nil 329 ref 659 ref 324 ref 655 ref 163 ref 370 remove 660 ref appTerm 668 def appTerm 163 ref 661 ref 29 ref 166 ref appTerm 657 ref appTerm 669 def appTerm 670 def appTerm 168 remove 662 ref appTerm 671 def appTerm 672 def appTerm 673 def absTerm 674 def appTerm 675 def absTerm nil cons cons nil cons nil cons cons 339 ref subst 659 remove nil 11 ref 675 remove nil cons cons nil cons nil cons cons 196 ref subst nil 329 ref 674 remove nil cons cons nil cons nil cons cons 339 ref subst 655 remove nil 11 ref 673 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 668 remove nil cons 676 def cons 677 def 162 ref 672 remove nil cons 678 def cons nil cons cons nil cons cons 679 def 179 ref subst 679 remove 237 ref subst nil 161 ref 670 ref nil cons 680 def cons 162 ref 671 remove nil cons 681 def cons nil cons cons nil cons cons 682 def 179 ref subst 682 remove 237 ref subst nil 619 remove 162 ref 662 ref nil cons 683 def cons nil cons cons nil cons cons 684 def 631 ref subst 684 ref 179 ref subst 684 remove 237 ref subst nil 161 ref 660 ref nil cons 685 def cons 686 def 162 ref 657 ref nil cons 687 def cons nil cons 688 def cons nil cons cons 689 def 179 ref subst 689 ref 237 ref subst nil 677 ref 162 ref 165 ref 660 remove appTerm 690 def nil cons 691 def cons nil cons cons nil cons cons 224 ref subst nil 161 ref 191 remove cons 162 ref 685 ref cons nil cons cons nil cons cons 692 def 381 ref subst eqMp 693 def nil 161 ref 691 ref cons 694 def 688 ref cons nil cons cons 695 def 224 ref subst proveHyp nil 677 remove 162 ref 661 remove 164 ref appTerm 696 def nil cons 697 def cons nil cons cons nil cons cons 224 ref subst 692 ref nil 373 remove 622 remove cons nil cons cons 698 def 179 ref subst 698 remove 237 ref subst 626 remove eqMp nil 379 remove 629 remove cons nil cons cons 216 ref subst deductAntisym eqMp 699 def subst eqMp 700 def nil 161 ref 697 ref cons 701 def 162 ref 163 ref 690 ref appTerm 702 def 657 ref appTerm nil cons 703 def cons nil cons cons nil cons cons 704 def 224 ref subst proveHyp 704 ref 179 ref subst 704 remove 237 ref subst 695 ref 179 ref subst 695 remove 237 ref subst nil 686 ref 627 remove cons nil cons cons 224 ref subst 696 remove assume eqMp 705 def 692 remove 224 ref subst 690 remove assume eqMp 706 def 705 remove proveHyp proveHyp nil 686 remove 162 ref 669 remove nil cons 707 def cons nil cons cons nil cons cons 224 ref subst 670 remove assume eqMp 708 def nil 161 ref 707 remove cons 709 def 162 ref 620 ref 657 ref appTerm 710 def nil cons 711 def cons nil cons cons nil cons cons 224 ref subst proveHyp nil 623 remove 688 ref cons nil cons cons 712 def 381 remove subst eqMp 713 def nil 161 ref 711 ref cons 714 def 688 remove cons nil cons cons 715 def 224 ref subst proveHyp 708 remove nil 709 remove 162 ref 163 ref 657 ref appTerm 166 ref appTerm 716 def nil cons 717 def cons nil cons cons nil cons cons 224 ref subst proveHyp 712 ref 699 remove subst eqMp 718 def nil 161 ref 717 ref cons 719 def 162 ref 163 ref 710 ref appTerm 720 def 657 remove appTerm nil cons 721 def cons nil cons cons nil cons cons 722 def 224 ref subst proveHyp 722 ref 179 ref subst 722 remove 237 ref subst 715 ref 179 ref subst 715 remove 237 ref subst 223 remove 712 remove 224 ref subst 710 remove assume eqMp proveHyp eqMp nil 201 ref 711 remove cons 723 def 202 ref 687 ref cons nil cons 724 def cons nil cons cons 216 ref subst deductAntisym eqMp eqMp nil 201 ref 717 remove cons 725 def 202 ref 721 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 201 ref 691 remove cons 726 def 724 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp nil 201 ref 697 remove cons 727 def 202 ref 703 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 201 ref 685 ref cons 724 remove cons nil cons cons 216 ref subst deductAntisym eqMp eqMp nil 628 remove 202 ref 683 ref cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp nil 161 ref 163 ref 167 ref appTerm 662 ref appTerm nil cons cons 162 ref 163 ref 662 ref appTerm 167 remove appTerm nil cons cons nil cons cons nil cons cons 237 ref subst proveHyp nil 161 ref 683 ref cons 375 remove cons nil cons cons 728 def 179 ref subst 728 remove 237 ref subst 179 ref 237 ref 693 remove nil 694 remove 624 ref cons nil cons cons 729 def 224 ref subst proveHyp 700 remove nil 701 remove 162 ref 702 remove 166 ref appTerm nil cons 730 def cons nil cons cons nil cons cons 731 def 224 ref subst proveHyp 731 ref 179 ref subst 731 remove 237 ref subst 729 ref 179 ref subst 729 remove 237 ref subst 706 remove 713 remove nil 714 remove 624 ref cons nil cons cons 732 def 224 ref subst proveHyp 718 remove nil 719 remove 162 ref 720 remove 166 remove appTerm nil cons 733 def cons nil cons cons nil cons cons 734 def 224 ref subst proveHyp 734 ref 179 ref subst 734 remove 237 ref subst 732 ref 179 ref subst 732 remove 237 ref subst 689 remove 224 ref subst 662 remove assume eqMp nil 161 ref 687 ref cons 624 remove cons nil cons cons 224 ref subst 716 remove assume eqMp proveHyp eqMp nil 723 remove 203 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp nil 725 remove 202 ref 733 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 726 remove 203 remove cons nil cons cons 216 ref subst deductAntisym eqMp eqMp nil 727 remove 202 ref 730 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp eqMp 217 remove deductAntisym eqMp eqMp nil 201 ref 683 remove cons 380 remove cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 201 ref 680 remove cons 202 ref 681 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp eqMp nil 201 ref 676 remove cons 202 ref 678 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp subst nil 161 ref 324 ref 666 ref appTerm nil cons cons 162 ref 667 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 666 remove nil cons cons 382 ref 685 remove cons nil cons cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 665 remove nil cons cons 162 ref 664 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 663 remove nil cons cons 382 ref 687 remove cons nil cons cons nil cons cons 244 ref subst eqMp eqMp subst eqMp subst eqMp 611 remove 11 ref 29 ref 163 ref 192 ref appTerm 37 ref appTerm appTerm 37 ref appTerm absTerm 735 def 192 ref appTerm 736 def betaConv nil 324 ref 735 ref appTerm 737 def axiom nil 161 ref 737 remove nil cons cons 162 ref 736 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 735 remove nil cons cons 421 ref cons nil cons cons 244 ref subst eqMp eqMp subst trans sym 195 ref eqMp 738 def subst eqMp eqMp nil 161 ref 146 ref 543 ref appTerm nil cons cons 162 ref 544 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 349 ref 228 ref 543 remove nil cons cons 232 ref 535 ref nil cons cons nil cons 739 def cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 542 remove nil cons cons 162 ref 541 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 225 ref 226 ref 540 remove nil cons cons 227 ref cons nil cons cons 244 ref subst eqMp eqMp sym 740 def subst subst 741 def appThm eqMp 70 ref 63 ref appTerm refl 70 ref "_29234" 16 ref var 742 def 490 ref 742 remove varTerm appTerm absTerm 743 def 65 ref appTerm 744 def appTerm refl 743 ref 508 ref appTerm betaConv appThm 70 ref refl 745 def 744 remove betaConv appThm 509 ref refl appThm trans 743 remove refl 524 remove 525 remove 144 ref 141 ref 51 ref 1 ref 1 ref 1 ref 529 ref 134 ref cons opType 746 def 4 ref cons opType 747 def 746 ref nil cons 748 def cons opType constTerm "fn" 746 ref var 749 def 146 ref 534 ref 159 ref 144 ref 141 ref 749 ref varTerm 536 ref appTerm appTerm 750 def 145 ref appTerm absTerm appTerm absTerm appTerm absTerm 751 def appTerm 752 def 536 ref appTerm appTerm 145 ref appTerm absTerm 753 def 145 ref appTerm 754 def betaConv 534 ref 159 ref 753 ref appTerm 755 def absTerm 756 def 535 ref appTerm 757 def betaConv 751 ref 752 remove appTerm 758 def betaConv 98 ref 1 ref 747 ref 4 ref cons opType constTerm 759 def refl 749 remove 547 remove 534 ref 548 remove 144 ref 750 remove refl 534 ref 144 ref 145 ref absTerm 760 def absTerm 761 def 535 ref appTerm betaConv 551 remove appThm 760 remove 145 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 134 ref cons nil cons "_1343" 1 ref 93 ref 135 ref cons opType var 761 remove nil cons cons nil cons nil cons cons 589 remove subst eqMp nil 161 ref 759 remove 751 ref appTerm nil cons cons 162 ref 758 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp "A" 748 remove cons nil cons "p" 747 remove var 751 remove nil cons cons nil cons nil cons cons 738 ref subst eqMp eqMp nil 161 ref 146 ref 756 ref appTerm nil cons cons 162 ref 757 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 349 ref 228 ref 756 remove nil cons cons 739 ref cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 755 remove nil cons cons 162 ref 754 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 225 ref 226 ref 753 remove nil cons cons 227 ref cons nil cons cons 244 ref subst eqMp eqMp sym 762 def subst subst 763 def appThm eqMp appThm nil 487 remove 64 ref nil cons 764 def cons 474 ref 63 ref nil cons 765 def cons nil cons cons nil cons cons 766 def 301 ref "B" 14 ref cons nil cons 767 def cons 92 ref cons 768 def 740 ref subst subst eqMp 769 def appThm eqMp 70 ref 64 ref appTerm refl 70 ref "_29236" 16 remove var 770 def 495 ref 770 remove varTerm appTerm absTerm 771 def 65 remove appTerm 772 def appTerm refl 771 ref 508 remove appTerm betaConv appThm 745 ref 772 remove betaConv appThm 514 ref refl appThm trans 771 remove refl 763 remove appThm eqMp appThm 766 remove 768 remove 762 ref subst subst eqMp 773 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 52 remove cons nil cons 774 def "P" 39 ref var 460 ref nil cons 775 def cons "x" 38 remove var 496 remove nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp nil 161 ref 98 ref 1 ref 39 ref 4 ref cons opType constTerm 460 remove appTerm nil cons cons 162 ref 470 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp nil "p" 39 remove var 775 remove cons nil cons nil cons cons 774 remove 92 ref cons 738 ref subst subst eqMp eqMp nil 161 ref 7 ref 468 ref appTerm nil cons cons 162 ref 469 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 468 remove nil cons cons 455 ref 764 remove cons nil cons 776 def cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 467 remove nil cons cons 162 ref 466 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 465 remove nil cons cons 455 ref 765 remove cons nil cons 777 def cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 464 remove nil cons cons 162 ref 463 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 462 remove nil cons cons 455 ref 523 remove cons nil cons 778 def cons nil cons cons 244 ref subst eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 7 ref 449 remove appTerm thm nil 300 ref 9 ref 43 ref 44 ref 29 ref "Number.Natural.Prime.Sieve.invariant" "_29248" 13 ref 2 ref 46 ref cons opType 779 def var 780 def 27 ref 68 ref 70 ref "Data.Pair.fst" const 781 def 1 ref 779 ref 14 ref cons opType constTerm 782 def 780 ref varTerm 783 def appTerm 784 def appTerm 71 ref appTerm appTerm appTerm 27 ref 28 ref 1 ref 12 ref 14 ref opType 785 def 1 ref 785 ref 4 ref cons opType nil cons cons opType constTerm 786 def "Data.List.map" const 787 def 1 ref 472 ref 1 ref 21 ref 785 ref nil cons 788 def cons opType nil cons cons opType constTerm 781 ref 472 ref constTerm 789 def appTerm 790 def "Data.Pair.snd" const 791 def 1 ref 779 ref 46 ref cons opType constTerm 792 def 783 ref appTerm 793 def appTerm appTerm "Number.Natural.Prime.below" const 1 ref 2 ref 788 ref cons opType constTerm 794 def 76 ref 784 ref appTerm "Number.Natural.bit1" const 73 ref constTerm 795 def 71 ref appTerm 796 def appTerm appTerm appTerm appTerm 413 ref 784 remove appTerm 71 ref appTerm 793 remove appTerm appTerm appTerm absTerm 797 def defineConst 798 def pop 1 ref 779 ref 4 ref cons opType 799 def constTerm 800 def 58 ref 1 ref 2 ref 1 ref 21 ref 779 ref nil cons 801 def cons opType nil cons cons opType constTerm 802 def 31 ref appTerm 49 ref appTerm 803 def appTerm appTerm 27 ref 68 ref 70 ref 31 ref appTerm 71 ref appTerm appTerm appTerm 804 def 27 ref 786 ref 790 ref 49 ref appTerm appTerm 794 ref 76 ref 31 ref appTerm 796 ref appTerm 805 def appTerm 806 def appTerm appTerm 414 remove 71 ref appTerm 807 def 49 ref appTerm appTerm appTerm appTerm 808 def absTerm 809 def appTerm 810 def absTerm 811 def nil cons cons nil cons nil cons cons 304 ref subst 9 ref nil 11 ref 810 remove nil cons cons nil cons nil cons cons 196 ref subst nil 312 ref 809 remove nil cons cons nil cons nil cons cons 314 ref subst 44 ref nil 11 ref 808 remove nil cons cons nil cons nil cons cons 196 ref subst nil 780 remove 803 ref nil cons cons nil cons nil cons cons 798 remove 783 ref refl appThm 797 remove 783 remove appTerm betaConv trans subst 29 ref "_29254" 21 ref var 812 def 804 remove 27 ref 786 ref 790 ref 812 ref varTerm 813 def appTerm appTerm 814 def 806 remove appTerm appTerm 807 remove 813 ref appTerm appTerm appTerm absTerm 49 ref appTerm 815 def appTerm refl 812 ref 27 ref 68 ref 70 ref 782 ref 803 ref appTerm 816 def appTerm 71 ref appTerm appTerm appTerm 817 def 27 ref 814 ref 794 ref 76 ref 816 ref appTerm 796 ref appTerm appTerm 818 def appTerm appTerm 413 ref 816 ref appTerm 71 ref appTerm 819 def 813 ref appTerm appTerm appTerm absTerm 820 def 792 ref 803 ref appTerm 821 def appTerm betaConv appThm 204 ref 815 remove betaConv appThm 817 remove 27 ref 786 ref 790 ref 821 ref appTerm appTerm 818 remove appTerm appTerm 819 remove 821 remove appTerm appTerm appTerm refl appThm trans 28 ref 1 ref 22 remove 42 remove nil cons cons opType constTerm 822 def "_29253" 2 ref var 823 def 812 remove 27 ref 68 ref 70 ref 823 remove varTerm 824 def appTerm 71 ref appTerm appTerm appTerm 27 ref 814 remove 794 ref 76 ref 824 ref appTerm 796 ref appTerm appTerm appTerm appTerm 413 remove 824 remove appTerm 71 ref appTerm 813 remove appTerm appTerm appTerm absTerm absTerm 825 def 31 ref appTerm 826 def appTerm refl 825 ref 816 remove appTerm betaConv appThm 822 remove refl 826 remove betaConv appThm 820 remove refl appThm trans 825 remove refl nil "b" 21 ref var 318 remove cons 474 remove 456 remove cons nil cons cons nil cons cons 827 def "B" 46 ref cons 828 def 302 ref cons 92 ref cons 144 ref 527 ref 781 remove 530 remove constTerm 536 ref appTerm appTerm 535 ref appTerm absTerm 829 def 145 ref appTerm 830 def betaConv 534 ref 159 ref 829 ref appTerm 831 def absTerm 832 def 535 ref appTerm 833 def betaConv nil 146 ref 832 ref appTerm 834 def axiom nil 161 ref 834 remove nil cons cons 162 ref 833 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 349 ref 228 ref 832 remove nil cons cons 739 ref cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 831 remove nil cons cons 162 ref 830 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 225 ref 226 ref 829 remove nil cons cons 227 ref cons nil cons cons 244 ref subst eqMp eqMp subst subst sym appThm eqMp 827 remove 301 remove 828 remove nil cons cons 92 ref cons 144 ref 141 ref 791 remove 746 remove constTerm 536 ref appTerm appTerm 145 ref appTerm absTerm 835 def 145 remove appTerm 836 def betaConv 534 ref 159 remove 835 ref appTerm 837 def absTerm 838 def 535 remove appTerm 839 def betaConv nil 146 ref 838 ref appTerm 840 def axiom nil 161 ref 840 remove nil cons cons 162 ref 839 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 349 ref 228 ref 838 remove nil cons cons 739 remove cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 837 remove nil cons cons 162 ref 836 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 225 remove 226 remove 835 remove nil cons cons 227 remove cons nil cons cons 244 ref subst eqMp eqMp subst subst sym appThm eqMp sym trans 841 def eqMp absThm eqMp eqMp absThm eqMp nil 7 ref 811 remove appTerm thm nil "P" 799 ref var 842 def "r" 779 ref var 843 def 29 ref 800 ref 843 ref varTerm 844 def appTerm appTerm 28 ref 1 ref 779 ref 799 ref nil cons cons opType constTerm "Number.Natural.Prime.Sieve.sieve" "Number.Natural.Prime.Sieve.mk" "Number.Natural.Prime.Sieve.dest" nil "A" 801 ref cons nil cons 845 def 92 ref cons 846 def 105 ref subst "n_ps" 779 ref var 847 def 800 remove 847 remove varTerm appTerm absTerm 848 def refl appThm "p" 799 ref var 849 def 849 remove varTerm 850 def 51 ref 1 ref 799 ref 801 ref cons opType constTerm 850 remove appTerm appTerm absTerm 848 ref appTerm betaConv trans 848 ref 802 ref 796 ref appTerm 36 ref appTerm 851 def appTerm betaConv sym nil 44 ref 36 ref nil cons cons 9 ref 796 ref nil cons cons nil cons 852 def cons nil cons cons 841 remove subst 401 ref 68 ref refl 745 ref nil 9 ref 71 ref nil cons 853 def cons nil cons nil cons cons 854 def 9 ref 70 ref 795 remove 31 ref appTerm appTerm "Number.Natural.suc" const 73 ref constTerm 855 def "Number.Natural.bit0" const 73 remove constTerm 856 def 31 ref appTerm appTerm 857 def appTerm absTerm 858 def 31 ref appTerm 859 def betaConv nil 7 ref 858 ref appTerm 860 def axiom nil 161 ref 860 remove nil cons cons 162 ref 859 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 858 remove nil cons cons 457 ref cons nil cons cons 244 ref subst eqMp eqMp subst 855 ref refl 861 def nil 70 ref 856 ref 71 ref appTerm appTerm 71 ref appTerm axiom appThm 862 def trans 863 def appThm 854 ref 306 ref subst appThm 854 ref 9 ref 68 ref 70 ref 855 ref 31 ref appTerm 864 def appTerm 71 ref appTerm 865 def appTerm 866 def absTerm 867 def 31 ref appTerm 868 def betaConv nil 7 ref 867 ref appTerm 869 def axiom nil 161 ref 869 remove nil cons cons 162 ref 868 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 867 remove nil cons cons 457 ref cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 866 remove nil cons cons 162 ref 29 ref 865 ref appTerm "Data.Bool.F" const 3 ref constTerm 870 def appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp nil 201 ref 865 remove nil cons cons nil cons nil cons cons nil 161 ref 68 ref 205 ref appTerm 871 def nil cons 872 def cons 162 ref 29 ref 205 ref appTerm 870 ref appTerm nil cons 873 def cons nil cons cons nil cons cons 874 def 179 ref subst 874 remove 237 ref subst nil 161 ref 205 ref nil cons 875 def cons 162 ref 870 ref nil cons 876 def cons nil cons cons nil cons cons 631 remove subst 29 ref 871 ref appTerm refl 161 ref 165 ref 870 ref appTerm absTerm 877 def 205 ref appTerm betaConv appThm nil 187 ref 68 ref appTerm 877 remove appTerm axiom 214 ref appThm eqMp 871 remove assume eqMp nil 161 ref 163 ref 205 ref appTerm 878 def 870 ref appTerm nil cons cons 162 ref 163 ref 870 ref appTerm 205 ref appTerm nil cons cons nil cons cons nil cons cons 237 ref subst proveHyp nil 161 ref 876 ref cons 162 ref 875 ref cons nil cons cons nil cons cons 879 def 179 ref subst 879 remove 237 ref subst 161 ref 164 remove absTerm 880 def 205 ref appTerm 881 def betaConv nil 29 ref 870 ref appTerm 324 ref 880 ref appTerm 882 def appTerm axiom 870 ref assume eqMp nil 161 ref 882 remove nil cons cons 162 ref 881 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 880 remove nil cons cons 382 ref 875 ref cons nil cons cons nil cons cons 244 ref subst eqMp eqMp eqMp nil 201 ref 876 remove cons 202 ref 875 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 201 ref 872 remove cons 202 ref 873 remove cons nil cons cons nil cons cons 216 ref subst deductAntisym eqMp subst eqMp subst trans appThm nil 29 ref 68 ref 870 ref appTerm 883 def appTerm 37 ref appTerm axiom 884 def trans appThm 401 ref 786 ref 790 ref 36 ref appTerm appTerm 885 def refl 794 ref refl 886 def 76 ref refl 863 ref appThm 863 ref appThm nil 9 ref 855 ref 71 ref appTerm 887 def nil cons cons 888 def "m" 2 ref var 889 def 853 ref cons nil cons cons nil cons cons 9 ref 70 ref 76 ref 855 ref 889 ref varTerm 890 def appTerm appTerm 31 ref appTerm appTerm 855 ref 76 ref 890 ref appTerm 31 ref appTerm appTerm appTerm absTerm 891 def 31 ref appTerm 892 def betaConv 889 remove 7 ref 891 ref appTerm 893 def absTerm 894 def 890 ref appTerm 895 def betaConv nil 7 ref 894 ref appTerm 896 def axiom nil 161 ref 896 remove nil cons cons 162 ref 895 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 894 remove nil cons cons 455 ref 890 remove nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 893 remove nil cons cons 162 ref 892 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 891 remove nil cons cons 457 ref cons nil cons cons 244 ref subst eqMp eqMp subst 861 ref nil 888 remove nil cons nil cons cons 9 ref 70 ref 76 ref 71 ref appTerm 31 ref appTerm appTerm 31 ref appTerm absTerm 897 def 31 ref appTerm 898 def betaConv nil 7 ref 897 ref appTerm 899 def axiom nil 161 ref 899 remove nil cons cons 162 ref 898 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 897 remove nil cons cons 457 ref cons nil cons cons 244 ref subst eqMp eqMp subst appThm trans trans appThm appThm appThm nil 10 ref 853 remove cons 852 remove cons nil cons cons 417 remove 196 ref subst 433 ref 33 ref appTerm 900 def betaConv 435 ref 31 ref appTerm 901 def betaConv 432 remove nil 161 ref 436 remove nil cons cons 162 ref 901 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 435 remove nil cons cons 457 ref cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 434 remove nil cons cons 162 ref 900 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 433 remove nil cons cons 458 ref cons nil cons cons 244 ref subst eqMp eqMp eqMp subst appThm nil 11 ref 885 remove 794 ref 855 ref 887 ref appTerm 902 def appTerm appTerm nil cons cons nil cons nil cons cons 903 def 11 ref 29 ref 27 ref 192 ref appTerm 37 ref appTerm appTerm 192 ref appTerm absTerm 904 def 192 ref appTerm 905 def betaConv nil 324 ref 904 ref appTerm 906 def axiom nil 161 ref 906 remove nil cons cons 162 ref 905 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 904 remove nil cons cons 421 ref cons nil cons cons 244 ref subst eqMp eqMp subst trans appThm 903 remove 11 ref 29 ref 27 ref 37 ref appTerm 192 ref appTerm appTerm 192 ref appTerm absTerm 907 def 192 remove appTerm 908 def betaConv nil 324 ref 907 ref appTerm 909 def axiom nil 161 ref 909 remove nil cons cons 162 ref 908 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 907 remove nil cons cons 421 remove cons nil cons cons 244 ref subst eqMp eqMp subst trans trans sym 786 ref refl nil "f" 472 remove var 789 remove nil cons cons nil cons nil cons cons 131 ref 767 remove cons 92 ref cons "f" 599 ref var 910 def 28 ref 1 ref 12 remove 134 remove opType 911 def 1 ref 911 ref 4 ref cons opType nil cons cons opType constTerm 787 remove 1 ref 599 ref 1 ref 132 remove 911 ref nil cons cons opType nil cons cons opType constTerm 910 ref varTerm 912 def appTerm 143 remove appTerm appTerm 35 ref 911 remove constTerm appTerm absTerm 913 def 912 ref appTerm 914 def betaConv nil 606 ref 913 ref appTerm 915 def axiom nil 161 ref 915 remove nil cons cons 162 ref 914 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 608 remove 609 remove 913 remove nil cons cons 610 remove 912 ref nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp subst subst appThm 886 remove 861 ref 70 ref 887 ref appTerm 796 ref appTerm assume sym 70 ref 796 ref appTerm 887 remove appTerm assume sym deductAntisym 863 ref eqMp appThm 70 ref 855 ref 796 ref appTerm 916 def appTerm 856 ref 796 ref appTerm 917 def appTerm assume sym 70 ref 917 ref appTerm 916 remove appTerm assume sym deductAntisym 745 remove 856 ref refl 863 ref appThm 854 remove 9 ref 70 ref 856 remove 864 remove appTerm appTerm 855 remove 857 remove appTerm appTerm absTerm 918 def 31 ref appTerm 919 def betaConv nil 7 ref 918 ref appTerm 920 def axiom nil 161 ref 920 remove nil cons cons 162 ref 919 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 918 remove nil cons cons 457 ref cons nil cons cons 244 ref subst eqMp eqMp subst 861 ref 862 remove appThm trans trans appThm 861 remove 863 remove appThm appThm nil 455 remove 902 remove nil cons cons nil cons nil cons cons 303 remove nil 11 ref 527 ref 233 ref appTerm 233 ref appTerm nil cons cons nil cons nil cons cons 196 ref subst 243 remove eqMp 921 def subst subst trans sym 195 ref eqMp eqMp trans appThm nil 786 ref 794 remove 917 remove appTerm appTerm 35 remove 785 ref constTerm 922 def appTerm axiom trans appThm nil "x" 785 remove var 922 remove nil cons cons nil cons nil cons cons "A" 788 ref cons nil cons 92 ref cons 921 ref subst subst trans sym 195 ref eqMp eqMp eqMp 845 remove 842 remove 848 ref nil cons cons "x" 779 ref var 851 ref nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp eqMp defineTypeOp 923 def pop 924 def pop 925 def pop 926 def pop 927 def pop 925 remove 1 ref 927 remove nil opType 928 def 801 remove cons opType constTerm 929 def 926 remove 1 ref 779 ref 928 ref nil cons 930 def cons opType constTerm 931 def 844 ref appTerm appTerm appTerm 844 ref appTerm 932 def appTerm 933 def absTerm 934 def nil cons cons nil cons nil cons cons 846 remove 289 ref subst subst 843 ref nil 11 ref 933 remove nil cons cons nil cons nil cons cons 196 ref subst 204 ref 848 remove 844 ref appTerm 935 def betaConv appThm 932 ref refl appThm 204 ref 843 ref 932 remove absTerm 844 ref appTerm betaConv appThm 843 remove 935 remove absTerm 844 ref appTerm betaConv appThm 923 remove 844 remove refl appThm eqMp sym eqMp eqMp absThm eqMp nil 0 ref 1 ref 799 remove 4 ref cons opType constTerm 934 remove appTerm thm nil "P" 1 ref 928 ref 4 ref cons opType 936 def var 937 def "a" 928 ref var 938 def 28 ref 1 ref 928 ref 936 ref nil cons 939 def cons opType constTerm 940 def 931 ref 929 ref 938 ref varTerm 941 def appTerm appTerm 942 def appTerm 941 ref appTerm 943 def absTerm 944 def nil cons cons nil cons nil cons cons "A" 930 ref cons 945 def nil cons 946 def 92 ref cons 289 ref subst 947 def subst 938 ref nil 11 ref 943 remove nil cons cons nil cons nil cons cons 196 ref subst 940 ref refl 938 ref 942 remove absTerm 941 ref appTerm betaConv appThm 938 remove 941 ref absTerm 941 ref appTerm betaConv appThm 924 remove 941 remove refl appThm eqMp eqMp absThm eqMp nil 0 ref 1 ref 936 ref 4 ref cons opType 948 def constTerm 949 def 944 remove appTerm thm "Number.Natural.Prime.Sieve.initial" 931 ref 851 remove appTerm 950 def defineConst 951 def pop 952 def pop 951 remove nil 940 ref 952 remove 928 ref constTerm appTerm 950 remove appTerm thm nil 937 ref "s" 928 ref var 953 def 70 ref "Number.Natural.Prime.Sieve.max" "_29257" 928 ref var 954 def 782 ref 929 ref 954 ref varTerm 955 def appTerm appTerm 956 def absTerm 957 def defineConst 958 def pop 1 ref 928 ref 14 remove cons opType constTerm 959 def 953 ref varTerm 960 def appTerm appTerm 782 remove 929 ref 960 ref appTerm 961 def appTerm appTerm absTerm 962 def nil cons cons nil cons nil cons cons 947 ref subst 954 remove nil 11 ref 70 ref 959 ref 955 ref appTerm appTerm 956 remove appTerm nil cons cons nil cons nil cons cons 196 ref subst 958 remove 955 ref refl appThm 957 remove 955 remove appTerm betaConv trans eqMp absThm eqMp nil 949 ref 962 remove appTerm thm nil 937 ref 953 ref 786 ref "Number.Natural.Prime.Sieve.primes" "_29262" 928 ref var 963 def 790 ref 792 ref 929 ref 963 ref varTerm 964 def appTerm appTerm appTerm 965 def absTerm 966 def defineConst 967 def pop 1 ref 928 ref 788 remove cons opType constTerm 968 def 960 ref appTerm appTerm 790 remove 792 remove 961 ref appTerm appTerm appTerm absTerm 969 def nil cons cons nil cons nil cons cons 947 ref subst 963 remove nil 11 ref 786 remove 968 remove 964 ref appTerm appTerm 965 remove appTerm nil cons cons nil cons nil cons cons 196 ref subst 967 remove 964 ref refl appThm 966 remove 964 remove appTerm betaConv trans eqMp absThm eqMp nil 949 ref 969 remove appTerm thm "Number.Natural.Prime.Sieve.increment.inc" "inc_counters_sieve" 1 ref 2 ref 1 ref 2 ref 1 ref 21 ref 13 ref 3 ref 46 remove cons opType 970 def nil cons 971 def cons opType nil cons 972 def cons opType nil cons cons opType 973 def var 974 def nil cons cons nil cons 974 ref 27 ref 7 ref 9 ref 7 ref 10 ref 28 ref 1 ref 970 ref 1 ref 970 ref 4 ref cons opType nil cons cons opType constTerm 975 def 974 ref varTerm 976 def 31 ref appTerm 977 def 33 ref appTerm 978 def 36 ref appTerm appTerm 58 ref 1 ref 3 ref 972 remove cons opType constTerm 979 def 37 ref appTerm 47 ref 59 ref 31 ref appTerm 62 ref 71 ref appTerm 980 def 71 ref appTerm appTerm appTerm 36 ref appTerm appTerm 981 def appTerm absTerm appTerm absTerm appTerm appTerm 7 ref 9 ref 7 ref 10 ref 40 ref 41 ref 43 ref 44 ref 975 ref 978 remove 50 ref appTerm appTerm 51 ref 1 ref 1 ref 1 ref 19 ref 971 ref cons opType 982 def 4 ref cons opType 983 def 982 ref nil cons 984 def cons opType constTerm 985 def "f" 982 ref var 986 def 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 975 ref 986 ref varTerm 66 ref appTerm appTerm 987 def "k'" 2 ref var 988 def "j'" 2 ref var 989 def "Data.Bool.cond" const 990 def 1 ref 3 ref 1 ref 970 ref 1 ref 970 ref 971 ref cons opType 991 def nil cons 992 def cons opType nil cons cons opType constTerm 70 remove 988 ref varTerm 993 def appTerm 71 ref appTerm appTerm 994 def 979 ref 870 ref appTerm 995 def 47 ref 61 ref 980 remove 989 ref varTerm 996 def appTerm 997 def appTerm appTerm 998 def 49 ref appTerm appTerm appTerm 999 def 51 ref 1 ref 1 ref 991 ref 4 ref cons opType 992 remove cons opType constTerm 1000 def "f" 991 remove var 1001 def 324 ref "b" 3 ref var 1002 def 43 ref "ps'" 21 ref var 1003 def 975 ref 1001 ref varTerm 979 remove 1002 ref varTerm 1004 def appTerm 1005 def 1003 ref varTerm 1006 def appTerm 1007 def appTerm appTerm 1008 def 1005 ref 47 ref 61 remove 62 remove 993 remove appTerm 71 remove appTerm 1009 def appTerm appTerm 1006 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1010 def 977 remove 996 ref appTerm 49 ref appTerm appTerm appTerm absTerm 76 ref 64 ref appTerm 33 ref appTerm 1011 def appTerm absTerm 77 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 48 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 1012 def refl 1013 def 28 ref 1 ref 973 ref 1 ref 973 ref 4 ref cons opType 1014 def nil cons cons opType constTerm 1015 def 976 ref appTerm 1016 def 51 ref 1 ref 1014 ref 973 ref nil cons 1017 def cons opType constTerm 1018 def 1012 ref appTerm appTerm assume sym appThm 1012 ref 976 ref appTerm betaConv 1019 def trans "A" 1017 remove cons nil cons 1020 def 92 ref cons 105 ref subst 1013 remove appThm "p" 1014 ref var 1021 def 1021 remove varTerm 1022 def 1018 remove 1022 remove appTerm appTerm absTerm 1012 ref appTerm betaConv trans 98 ref 1 ref 1 ref 1 ref 21 ref 1 ref 2 ref 1 ref 2 ref 971 remove cons opType 1023 def nil cons cons opType 1024 def nil cons 1025 def cons opType 1026 def 4 ref cons opType 1027 def 4 ref cons opType 1028 def constTerm 1029 def refl "fn" 1026 ref var 1030 def 27 ref 28 ref 1 ref 1024 ref 1 ref 1024 ref 4 ref cons opType nil cons cons opType constTerm 1031 def 1030 remove varTerm 1032 def 36 ref appTerm appTerm 9 ref 10 ref 981 ref absTerm 1033 def absTerm 1034 def appTerm appTerm refl 118 ref 119 ref 120 ref 121 ref 1031 ref 1032 ref 124 ref appTerm appTerm refl 41 ref 44 ref "_29271" 1024 ref var 1035 def 9 ref 10 ref 985 ref 986 ref 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 987 ref 988 ref 989 ref 999 ref 1010 ref 1035 ref varTerm 31 ref appTerm 996 ref appTerm appTerm 1036 def appTerm absTerm 1011 ref appTerm absTerm 77 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1037 def 48 ref appTerm absTerm absTerm absTerm absTerm absTerm 1038 def 122 ref appTerm betaConv 128 remove appThm 44 ref 1035 ref 9 ref 10 ref 1037 remove 122 ref appTerm absTerm absTerm absTerm absTerm 123 ref appTerm betaConv trans 1032 remove 123 ref appTerm 1039 def refl appThm 1035 remove 9 ref 10 ref 985 ref 986 ref 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 987 ref 988 ref 989 ref 994 ref 995 ref 998 remove 123 ref appTerm appTerm appTerm 1040 def 1036 remove appTerm absTerm 1011 ref appTerm absTerm 77 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 122 ref appTerm absTerm absTerm absTerm 1039 remove appTerm betaConv trans appThm absThm appThm absThm appThm appThm absThm appThm nil "f" 1 ref 19 ref 1 ref 21 ref 1 ref 1024 ref 1025 ref cons opType nil cons cons opType nil cons cons opType var 1038 remove nil cons cons "b" 1024 remove var 1034 ref nil cons cons nil cons cons nil cons cons 131 remove "B" 1025 remove cons nil cons cons 92 ref cons 245 remove subst subst eqMp nil 161 ref 1029 ref "_29270" 1026 ref var 1041 def 27 ref 1031 ref 1041 ref varTerm 1042 def 36 ref appTerm 1043 def appTerm 1034 ref appTerm 1044 def appTerm 1045 def 40 ref 41 ref 43 ref 44 ref 1031 ref 1042 ref 50 ref appTerm 1046 def appTerm 9 ref 10 ref 985 ref 986 ref 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 987 ref 988 ref 989 ref 999 ref 1010 ref 1042 ref 49 ref appTerm 31 ref appTerm 996 ref appTerm appTerm appTerm absTerm 1011 ref appTerm absTerm 77 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 48 ref appTerm 1047 def absTerm 1048 def absTerm 1049 def appTerm absTerm 1050 def appTerm 1051 def absTerm 1052 def appTerm 1053 def appTerm 1054 def absTerm 1055 def appTerm 1056 def nil cons cons 162 ref 1029 remove 1041 ref 27 remove 7 ref 9 ref 7 ref 10 ref 975 ref 1043 remove 31 ref appTerm 1057 def 33 ref appTerm appTerm 1058 def 981 ref appTerm 1059 def absTerm 1060 def appTerm 1061 def absTerm 1062 def appTerm 1063 def appTerm 7 ref 9 ref 7 ref 10 ref 40 ref 41 ref 43 ref 44 ref 975 ref 1046 remove 31 ref appTerm 1064 def 33 ref appTerm appTerm 1065 def 1047 remove appTerm 1066 def absTerm 1067 def appTerm 1068 def absTerm 1069 def appTerm 1070 def absTerm 1071 def appTerm 1072 def absTerm 1073 def appTerm 1074 def appTerm 1075 def absTerm 1076 def appTerm 1077 def nil cons 1078 def cons nil cons 1079 def cons nil cons cons 224 ref subst nil "P" 1027 remove var 1080 def 1041 ref 163 ref 1055 ref 1042 ref appTerm 1081 def appTerm 1077 ref appTerm 1082 def absTerm nil cons cons nil cons nil cons cons "A" 1026 ref nil cons cons nil cons 1083 def 92 ref cons 289 ref subst 1084 def subst 1041 ref nil 11 ref 1082 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 1081 remove nil cons 1085 def cons 1079 ref cons nil cons cons 1086 def 179 ref subst 1086 remove 237 ref subst 1041 ref 1045 remove 40 ref 119 remove 43 ref 121 remove 1031 ref 1042 ref 124 remove appTerm appTerm 9 ref 10 ref 985 ref 986 ref 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 987 ref 988 ref 989 ref 1040 remove 1010 ref 1042 ref 123 remove appTerm 31 ref appTerm 996 ref appTerm appTerm appTerm absTerm 1011 ref appTerm absTerm 77 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 122 remove appTerm absTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 1042 ref appTerm 1087 def betaConv 1087 remove assume eqMp nil 161 ref 1054 remove nil cons 1088 def cons 1079 remove cons nil cons cons 1089 def 224 ref subst proveHyp 1089 ref 179 ref subst 1089 remove 237 ref subst 1076 ref 1042 ref appTerm 1090 def betaConv 1091 def sym nil 201 ref 1044 ref nil cons cons 202 ref 1053 remove nil cons 1092 def cons nil cons cons nil cons cons 1093 def 216 ref subst nil 300 ref 1062 remove nil cons cons nil cons nil cons cons 304 ref subst 9 ref nil 11 ref 1061 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 1060 remove nil cons cons nil cons nil cons cons 304 ref subst 10 ref nil 11 ref 1059 remove nil cons cons nil cons nil cons cons 196 ref subst 1058 remove refl 1033 remove 33 ref appTerm betaConv appThm 28 ref 1 ref 1023 ref 1 ref 1023 remove 4 ref cons opType nil cons cons opType constTerm 1094 def 1057 remove appTerm refl 1034 remove 31 ref appTerm betaConv appThm 1044 remove assume 306 ref appThm eqMp 307 ref appThm eqMp eqMp absThm eqMp eqMp absThm eqMp proveHyp nil 161 ref 1063 remove nil cons cons 162 ref 1074 remove nil cons cons nil cons cons nil cons cons 237 ref subst proveHyp 1093 remove 308 ref subst nil 300 ref 1073 remove nil cons cons nil cons nil cons cons 304 ref subst 9 ref nil 11 ref 1072 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 1071 remove nil cons cons nil cons nil cons cons 304 ref subst 10 ref nil 11 ref 1070 remove nil cons cons nil cons nil cons cons 196 ref subst nil 309 ref 1069 remove nil cons cons nil cons nil cons cons 311 remove subst 41 ref nil 11 ref 1068 remove nil cons cons nil cons nil cons cons 196 ref subst nil 312 ref 1067 remove nil cons cons nil cons nil cons cons 314 ref subst 44 ref nil 11 ref 1066 remove nil cons cons nil cons nil cons cons 196 ref subst 1065 remove refl 1048 remove 33 ref appTerm betaConv appThm 1094 ref 1064 remove appTerm refl 1049 remove 31 ref appTerm betaConv appThm 1050 ref 49 ref appTerm 1095 def betaConv 1052 ref 48 ref appTerm 1096 def betaConv nil 161 ref 1092 remove cons 162 ref 1096 remove nil cons cons nil cons cons nil cons cons 224 ref subst 310 ref 309 ref 1052 remove nil cons cons 317 ref cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1051 remove nil cons cons 162 ref 1095 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 313 ref 312 ref 1050 remove nil cons cons 319 ref cons nil cons cons 244 ref subst eqMp eqMp 306 ref appThm eqMp 307 ref appThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp proveHyp eqMp eqMp 1083 ref 1080 ref 1076 ref nil cons cons 1097 def "x" 1026 remove var 1098 def 1042 ref nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp eqMp nil 201 ref 1088 remove cons 202 ref 1078 ref cons nil cons 1099 def cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp nil 201 ref 1085 remove cons 1099 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp nil 161 ref 0 ref 1028 remove constTerm 1100 def 1098 ref 163 ref 1055 ref 1098 ref varTerm 1101 def appTerm appTerm 1077 ref appTerm absTerm appTerm nil cons cons 162 ref 163 ref 1056 remove appTerm 1077 ref appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 1083 ref 1080 ref 1055 remove nil cons cons 1099 remove cons nil cons cons 383 ref subst eqMp eqMp proveHyp nil 161 ref 1078 remove cons 162 ref 98 ref 1 ref 1014 ref 4 ref cons opType constTerm 1012 ref appTerm 1102 def nil cons 1103 def cons nil cons 1104 def cons nil cons cons 224 ref subst nil 1080 remove 1041 ref 163 ref 1090 ref appTerm 1102 ref appTerm 1105 def absTerm nil cons cons nil cons nil cons cons 1084 remove subst 1041 remove nil 11 ref 1105 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 1090 ref nil cons 1106 def cons 1104 ref cons nil cons cons 1107 def 179 ref subst 1107 remove 237 ref subst 1091 remove 1090 remove assume eqMp nil 161 ref 1075 ref nil cons 1108 def cons 1104 ref cons nil cons cons 1109 def 224 ref subst proveHyp 1109 ref 179 ref subst 1109 remove 237 ref subst "_29267" 2 ref var 1110 def "_29268" 2 ref var 1111 def "_29269" 21 remove var 1112 def 1042 remove 1112 ref varTerm appTerm 1113 def 1110 remove varTerm appTerm 1111 ref varTerm 1114 def appTerm absTerm absTerm absTerm 1115 def refl nil 161 ref 1015 remove 1115 ref appTerm 1115 ref appTerm nil cons cons 1104 ref cons nil cons cons 224 ref subst proveHyp nil 974 remove 1115 ref nil cons cons nil cons nil cons cons nil 161 ref 1016 remove 1115 ref appTerm 1116 def nil cons 1117 def cons 1104 remove cons nil cons cons 1118 def 179 ref subst 1118 remove 237 ref subst 1019 remove sym 401 remove 8 ref 9 ref 8 ref 10 ref 975 ref refl 1119 def 1116 remove assume 306 remove appThm 1115 remove 31 ref appTerm betaConv trans 1120 def 307 remove appThm 1111 remove 1112 ref 1113 remove 31 ref appTerm 1121 def 1114 remove appTerm absTerm absTerm 1122 def 33 ref appTerm betaConv trans 1123 def 406 remove appThm 1112 ref 1121 ref 33 ref appTerm absTerm 1124 def 36 ref appTerm betaConv trans appThm 981 ref refl appThm absThm appThm absThm appThm appThm 8 ref 9 ref 8 ref 10 ref 118 remove 41 ref 120 remove 44 ref 1119 ref 1123 remove 408 remove appThm 1124 remove 50 ref appTerm betaConv trans appThm 985 ref refl 986 ref 8 ref 55 ref 8 ref 56 ref 8 remove 57 ref 987 ref refl 988 ref 989 ref 999 ref refl 1010 ref refl 1120 remove 996 ref refl appThm 1122 remove 996 ref appTerm betaConv trans 409 remove appThm 1112 remove 1121 remove 996 ref appTerm absTerm 49 ref appTerm betaConv trans appThm appThm absThm 1011 ref refl appThm absThm 77 ref refl appThm appThm absThm appThm absThm appThm absThm appThm absThm appThm 410 remove appThm appThm absThm appThm absThm appThm absThm appThm absThm appThm appThm sym 1075 remove assume eqMp eqMp 1020 remove "P" 1014 remove var 1012 remove nil cons cons "x" 973 ref var 976 remove nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp eqMp nil 201 ref 1117 remove cons 202 ref 1103 remove cons nil cons 1125 def cons nil cons cons 216 ref subst deductAntisym eqMp subst eqMp eqMp nil 201 ref 1108 remove cons 1125 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp nil 201 ref 1106 remove cons 1125 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp nil 161 ref 1100 remove 1098 remove 163 ref 1076 remove 1101 remove appTerm appTerm 1102 ref appTerm absTerm appTerm nil cons cons 162 ref 163 ref 1077 remove appTerm 1102 remove appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 1083 remove 1097 remove 1125 remove cons nil cons cons 383 ref subst eqMp eqMp proveHyp eqMp eqMp defineConstList 1126 def pop 1127 def pop 1126 ref nil 201 ref 7 ref 9 ref 7 ref 10 ref 975 ref 1127 remove hdTl pop 973 remove constTerm 1128 def 31 ref appTerm 1129 def 33 ref appTerm 1130 def 36 remove appTerm appTerm 981 remove appTerm absTerm appTerm absTerm appTerm 1131 def nil cons cons 202 ref 7 ref 9 ref 7 ref 10 ref 40 remove 41 remove 43 ref 44 ref 975 ref 1130 ref 50 remove appTerm appTerm 985 ref 986 remove 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 987 remove 988 ref 989 ref 999 remove 1010 remove 1129 remove 996 remove appTerm 49 ref appTerm 1132 def appTerm appTerm absTerm 1133 def 1011 remove appTerm absTerm 77 ref appTerm 1134 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 48 ref appTerm appTerm absTerm 1135 def appTerm 1136 def absTerm 1137 def appTerm 1138 def absTerm 1139 def appTerm 1140 def absTerm 1141 def appTerm nil cons 1142 def cons nil cons cons nil cons cons 1143 def 216 ref subst proveHyp nil 1131 remove thm nil 300 ref 9 ref 7 ref 10 ref 7 ref 57 ref 7 ref 56 ref 7 ref 55 ref 43 ref 44 ref 975 ref 1130 remove 437 remove appTerm appTerm 1134 ref appTerm 1144 def absTerm 1145 def appTerm 1146 def absTerm 1147 def appTerm 1148 def absTerm 1149 def appTerm 1150 def absTerm 1151 def appTerm 1152 def absTerm 1153 def appTerm 1154 def absTerm 1155 def nil cons cons nil cons nil cons cons 304 ref subst 9 ref nil 11 ref 1154 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 1153 remove nil cons cons nil cons nil cons cons 304 ref subst 10 remove nil 11 ref 1152 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 1151 remove nil cons cons nil cons nil cons cons 304 ref subst 57 ref nil 11 ref 1150 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 1149 remove nil cons cons nil cons nil cons cons 304 ref subst 56 ref nil 11 ref 1148 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 1147 remove nil cons cons nil cons nil cons cons 304 ref subst 55 ref nil 11 ref 1146 remove nil cons cons nil cons nil cons cons 196 ref subst nil 312 ref 1145 remove nil cons cons nil cons nil cons cons 314 remove subst 44 ref nil 11 ref 1144 remove nil cons cons nil cons nil cons cons 196 ref subst 1119 ref 450 remove 1135 ref 49 ref appTerm 1156 def betaConv 1137 ref 48 remove appTerm 1157 def betaConv 1139 ref 33 ref appTerm 1158 def betaConv 1141 ref 31 remove appTerm 1159 def betaConv 1126 remove 1143 remove 308 remove subst proveHyp nil 161 ref 1142 remove cons 162 ref 1159 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 1141 remove nil cons cons 457 remove cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1140 remove nil cons cons 162 ref 1158 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 1139 remove nil cons cons 458 remove cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1138 remove nil cons cons 162 ref 1157 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 310 remove 309 remove 1137 remove nil cons cons 317 remove cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1136 remove nil cons cons 162 ref 1156 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 313 remove 312 remove 1135 remove nil cons cons 319 remove cons nil cons cons 244 ref subst eqMp eqMp subst appThm 1134 ref refl appThm sym 57 ref 975 ref 985 remove "_29292" 982 ref var 1160 def 7 ref 55 ref 7 ref 56 ref 7 ref 57 ref 975 ref 1160 remove varTerm 66 ref appTerm appTerm 1134 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1161 def appTerm 1162 def 66 ref appTerm appTerm 1134 ref appTerm absTerm 1163 def 60 ref appTerm 1164 def betaConv 56 ref 7 ref 1163 ref appTerm 1165 def absTerm 1166 def 63 ref appTerm 1167 def betaConv 55 ref 7 ref 1166 ref appTerm 1168 def absTerm 1169 def 64 ref appTerm 1170 def betaConv 1161 ref 1162 remove appTerm 1171 def betaConv 1161 ref "_29290" 19 remove var 1172 def 988 ref 989 ref 994 ref 995 ref 47 ref 59 ref 481 remove 1172 remove varTerm 1173 def appTerm 1174 def appTerm 1175 def 997 ref appTerm appTerm 49 ref appTerm appTerm appTerm 1000 ref 1001 ref 324 ref 1002 ref 43 ref 1003 ref 1008 ref 1005 ref 47 ref 1175 remove 1009 ref appTerm appTerm 1006 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1132 ref appTerm appTerm absTerm 76 ref 495 remove 493 remove 1173 remove appTerm 1176 def appTerm appTerm 33 ref appTerm appTerm absTerm 75 ref 76 ref 490 remove 1176 remove appTerm appTerm 33 ref appTerm appTerm 1174 remove appTerm appTerm absTerm 1177 def appTerm betaConv sym nil 300 ref 55 ref 7 ref 56 ref 7 ref 57 ref 975 ref 1177 ref 66 remove appTerm 1178 def appTerm 1134 remove appTerm 1179 def absTerm 1180 def appTerm 1181 def absTerm 1182 def appTerm 1183 def absTerm nil cons cons nil cons nil cons cons 304 ref subst 55 remove nil 11 ref 1183 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 1182 remove nil cons cons nil cons nil cons cons 304 ref subst 56 remove nil 11 ref 1181 remove nil cons cons nil cons nil cons cons 196 ref subst nil 300 ref 1180 remove nil cons cons nil cons nil cons cons 304 remove subst 57 remove nil 11 ref 1179 remove nil cons cons nil cons nil cons cons 196 ref subst 1178 remove betaConv 975 remove "_29286" 2 ref var 1184 def 988 ref 1133 remove 76 ref 1184 ref varTerm appTerm 33 ref appTerm 1185 def appTerm absTerm 1186 def 77 remove appTerm absTerm 64 remove appTerm 1187 def appTerm refl 1184 ref 988 ref 989 ref 994 ref 995 ref 47 ref 59 ref 506 ref appTerm 1188 def 997 ref appTerm appTerm 49 ref appTerm appTerm appTerm 1000 ref 1001 ref 324 ref 1002 ref 43 ref 1003 ref 1008 ref 1005 ref 47 ref 1188 remove 1009 ref appTerm appTerm 1006 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1132 ref appTerm appTerm absTerm 1189 def 1185 ref appTerm absTerm 1190 def 510 ref appTerm absTerm 1191 def 514 ref appTerm betaConv appThm 1119 remove 1187 remove betaConv appThm 988 ref 1189 remove 76 ref 514 remove appTerm 33 ref appTerm appTerm absTerm 510 remove appTerm refl appThm trans 1094 ref "_29285" 2 ref var 1192 def 1184 ref 1186 remove 75 remove 76 remove 1192 ref varTerm appTerm 33 remove appTerm appTerm 1193 def 60 ref appTerm appTerm absTerm absTerm 63 remove appTerm 1194 def appTerm refl 1192 ref 1184 ref 1190 remove 1193 ref 506 ref appTerm appTerm absTerm absTerm 1195 def 509 remove appTerm betaConv appThm 1094 remove refl 1194 remove betaConv appThm 1191 remove refl appThm trans 1031 ref "_29284" 2 ref var 1196 def 1192 remove 1184 remove 988 remove 989 remove 994 remove 995 remove 47 ref 59 remove 1196 remove varTerm 1197 def appTerm 1198 def 997 remove appTerm appTerm 49 ref appTerm appTerm appTerm 1000 remove 1001 remove 324 ref 1002 ref 43 ref 1003 ref 1008 remove 1005 remove 47 remove 1198 remove 1009 remove appTerm appTerm 1006 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1132 remove appTerm appTerm absTerm 1185 remove appTerm absTerm 1193 remove 1197 remove appTerm appTerm absTerm absTerm absTerm 1199 def 60 remove appTerm 1200 def appTerm refl 1199 ref 506 remove appTerm betaConv appThm 1031 remove refl 1200 remove betaConv appThm 1195 remove refl appThm trans 1199 remove refl 741 remove appThm eqMp 769 remove appThm eqMp 773 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 984 remove cons nil cons 1201 def "P" 983 ref var 1161 ref nil cons 1202 def cons "x" 982 remove var 1177 remove nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp nil 161 ref 98 ref 1 ref 983 ref 4 ref cons opType constTerm 1161 remove appTerm nil cons cons 162 ref 1171 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp nil "p" 983 remove var 1202 remove cons nil cons nil cons cons 1201 remove 92 ref cons 738 ref subst subst eqMp eqMp nil 161 ref 7 ref 1169 ref appTerm nil cons cons 162 ref 1170 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 1169 remove nil cons cons 776 remove cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1168 remove nil cons cons 162 ref 1167 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 ref 300 ref 1166 remove nil cons cons 777 remove cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1165 remove nil cons cons 162 ref 1164 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 302 remove 300 remove 1163 remove nil cons cons 778 remove cons nil cons cons 244 ref subst eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 7 ref 1155 remove appTerm thm nil 937 ref 953 ref 28 ref 1 ref 13 ref 3 ref 930 ref cons opType 1203 def 1 ref 1203 ref 4 ref cons opType 1204 def nil cons 1205 def cons opType constTerm 1206 def "Number.Natural.Prime.Sieve.increment" "_29294" 928 ref var 1207 def 51 ref 1 ref 1 ref 1 ref 779 remove 1203 ref nil cons 1208 def cons opType 1209 def 4 ref cons opType 1209 ref nil cons cons opType constTerm "f" 1209 remove var 1210 def 7 remove 9 remove 43 ref 44 remove 1206 ref 1210 remove varTerm 803 remove appTerm appTerm "n'" 2 ref var 1211 def 51 ref 1 ref 1 ref 1 ref 970 remove 1208 ref cons opType 1212 def 4 ref cons opType 1212 ref nil cons cons opType constTerm "f" 1212 remove var 1213 def 324 ref 1002 ref 43 remove 1003 remove 1206 ref 1213 remove varTerm 1007 remove appTerm appTerm 58 ref 1 ref 3 ref 1 ref 928 ref 1208 ref cons opType 1214 def nil cons cons opType constTerm 1215 def 1004 ref appTerm 1216 def 931 remove 802 remove 1211 remove varTerm 1217 def appTerm 1006 remove appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1128 remove 1217 remove appTerm 796 remove appTerm 49 remove appTerm appTerm absTerm 805 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1218 def 929 remove 1207 ref varTerm 1219 def appTerm appTerm 1220 def absTerm 1221 def defineConst 1222 def pop 1214 remove constTerm 1223 def 960 ref appTerm 1224 def appTerm 1225 def 1218 remove 961 remove appTerm appTerm absTerm 1226 def nil cons cons nil cons nil cons cons 947 ref subst 1207 remove nil 11 ref 1206 ref 1223 remove 1219 ref appTerm appTerm 1220 remove appTerm nil cons cons nil cons nil cons cons 196 ref subst 1222 remove 1219 ref refl appThm 1221 remove 1219 remove appTerm betaConv trans eqMp absThm eqMp nil 949 ref 1226 remove appTerm thm "Number.Natural.Prime.Sieve.next" "fn" 1 ref 928 ref 13 remove 2 ref 930 ref cons opType 1227 def nil cons 1228 def cons opType 1229 def var 1230 def nil cons cons nil cons 1230 ref 949 ref 953 ref 28 ref 1 ref 1227 ref 1 ref 1227 ref 4 ref cons opType nil cons cons opType constTerm 1231 def 1230 ref varTerm 1232 def 960 ref appTerm appTerm 51 ref 1 ref 1 ref 1 ref 1203 ref 1228 ref cons opType 1233 def 4 ref cons opType 1234 def 1233 ref nil cons 1235 def cons opType constTerm 1236 def "f" 1233 ref var 1237 def 324 ref 1002 ref 949 ref "s'" 928 ref var 1238 def 1231 ref 1237 ref varTerm 1216 ref 1238 ref varTerm 1239 def appTerm 1240 def appTerm appTerm 1241 def 990 ref 1 ref 3 ref 1 ref 1227 ref 1 ref 1227 ref 1228 ref cons opType nil cons cons opType nil cons cons opType constTerm 1242 def 1004 ref appTerm 1243 def 58 remove 1 ref 2 remove 1229 ref nil cons 1244 def cons opType constTerm 1245 def 959 ref 1239 ref appTerm appTerm 1239 ref appTerm 1246 def appTerm 1247 def 1232 ref 1239 ref appTerm 1248 def appTerm 1249 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1224 ref appTerm 1250 def appTerm 1251 def absTerm 1252 def appTerm absTerm 1253 def refl 1254 def 28 ref 1 ref 1229 ref 1 ref 1229 ref 4 ref cons opType 1255 def nil cons cons opType constTerm 1256 def 1232 ref appTerm 51 ref 1 ref 1255 ref 1244 ref cons opType constTerm 1257 def 1253 ref appTerm appTerm assume sym appThm 1253 ref 1232 ref appTerm betaConv 1258 def trans "A" 1244 remove cons nil cons 1259 def 92 ref cons 1260 def 105 remove subst 1254 remove appThm "p" 1255 ref var 1261 def 1261 remove varTerm 1262 def 1257 remove 1262 remove appTerm appTerm absTerm 1253 ref appTerm betaConv trans "h" 1229 ref var 1263 def 98 ref 1 ref 1255 ref 4 ref cons opType 1264 def constTerm 1265 def "f" 1229 ref var 1266 def 949 ref "x" 928 ref var 1267 def 1231 ref 1266 ref varTerm 1268 def 1267 ref varTerm 1269 def appTerm appTerm 1270 def 1242 ref 953 ref 51 ref 1 ref 1 ref 1204 ref 4 ref cons opType 1271 def 1205 ref cons opType constTerm 1272 def "f" 1204 ref var 1273 def 324 ref 1002 ref 949 ref 1238 ref 29 ref 1273 ref varTerm 1240 ref appTerm appTerm 1274 def 68 ref 1004 ref appTerm 1275 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1224 ref appTerm 1276 def absTerm 1277 def 1269 ref appTerm appTerm 1278 def 1268 ref 953 ref 51 remove 1 ref 1 ref 1 ref 1203 ref 930 ref cons opType 1279 def 4 ref cons opType 1279 ref nil cons cons opType constTerm 1280 def "f" 1279 ref var 1281 def 324 ref 1002 ref 949 ref 1238 ref 940 ref 1281 ref varTerm 1240 ref appTerm appTerm 1282 def 1239 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1224 ref appTerm 1283 def absTerm 1284 def 1269 ref appTerm 1285 def appTerm appTerm 1286 def 1263 ref varTerm 1269 ref appTerm 1287 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm 1288 def 953 ref 1236 ref 1237 ref 324 ref 1002 ref 949 ref 1238 ref 1241 ref 1246 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1224 ref appTerm 1289 def absTerm 1290 def appTerm 1291 def betaConv "g" 1 ref 928 ref 930 ref cons opType 1292 def var 1293 def 0 ref 1264 remove constTerm 1294 def 1263 ref 1265 ref 1266 ref 949 ref 1267 ref 1270 ref 1278 ref 1268 remove 1293 ref varTerm 1269 ref appTerm appTerm 1295 def appTerm 1287 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1296 def 1284 ref appTerm 1297 def betaConv "p" 936 ref var 1298 def 0 ref 1 ref 1 ref 1292 ref 4 ref cons opType 1299 def 4 ref cons opType constTerm 1300 def 1293 remove 1294 ref 1263 remove 1265 ref 1266 ref 949 ref 1267 ref 1270 ref 1242 ref 1298 remove varTerm 1269 ref appTerm appTerm 1295 remove appTerm 1287 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1301 def 1277 ref appTerm 1302 def betaConv 945 remove "B" 1228 ref cons nil cons cons 92 ref cons nil 651 remove 101 remove 0 ref 1 ref 1 ref 1 ref 93 ref 103 remove cons opType 1303 def 4 ref cons opType 4 ref cons opType constTerm "g" 1303 ref var 1304 def 606 remove "h" 599 remove var 1305 def 98 ref 605 remove constTerm 910 remove 146 ref 232 ref 141 remove 912 ref 233 ref appTerm appTerm 990 ref 1 ref 3 ref 1 ref 133 remove 135 remove cons opType nil cons cons opType constTerm 325 remove appTerm 912 remove 1304 remove varTerm 233 ref appTerm appTerm appTerm 1305 remove varTerm 233 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm axiom subst nil 161 ref 0 ref 1 ref 948 ref 4 ref cons opType constTerm 1301 ref appTerm nil cons cons 162 ref 1302 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp "A" 939 remove cons nil cons "P" 948 ref var 1301 remove nil cons cons "x" 936 ref var 1277 ref nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1300 remove 1296 ref appTerm nil cons cons 162 ref 1297 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp "A" 1292 ref nil cons cons nil cons "P" 1299 remove var 1296 remove nil cons cons "x" 1292 remove var 1284 ref nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1294 ref 1288 ref appTerm nil cons cons 162 ref 1291 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 1259 ref "P" 1255 remove var 1306 def 1288 remove nil cons cons "x" 1229 ref var 1307 def 1290 ref nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1265 ref 1266 remove 949 ref 1267 ref 1270 remove 1286 remove 1290 ref 1269 ref appTerm 1308 def appTerm appTerm absTerm appTerm absTerm 1309 def appTerm 1310 def nil cons cons 162 ref 1265 remove 1253 ref appTerm 1311 def nil cons 1312 def cons nil cons 1313 def cons nil cons cons 224 ref subst proveHyp nil 1306 ref 1230 ref 163 ref 1309 ref 1232 ref appTerm 1314 def appTerm 1311 ref appTerm 1315 def absTerm nil cons cons nil cons nil cons cons 1260 remove 289 remove subst subst 1230 remove nil 11 ref 1315 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 1314 ref nil cons 1316 def cons 1313 ref cons nil cons cons 1317 def 179 ref subst 1317 remove 237 ref subst 1314 ref betaConv 1314 remove assume eqMp nil 161 ref 949 ref 1267 ref 1231 ref 1232 ref 1269 ref appTerm appTerm 1278 remove 1232 ref 1285 remove appTerm appTerm 1308 remove appTerm appTerm absTerm 1318 def appTerm nil cons 1319 def cons 1320 def 1313 remove cons nil cons cons 1321 def 224 ref subst proveHyp 1321 ref 179 ref subst 1321 remove 237 ref subst 1258 remove sym nil 937 ref 1252 remove nil cons cons nil cons nil cons cons 947 ref subst 953 ref nil 11 ref 1251 remove nil cons cons nil cons nil cons cons 196 ref subst 1231 ref refl 1322 def nil 1267 ref 960 ref nil cons cons nil cons nil cons cons 1318 ref 1269 ref appTerm 1323 def betaConv nil 1320 remove 162 ref 1323 remove nil cons cons nil cons cons nil cons cons 224 ref subst 946 ref 937 ref 1318 remove nil cons cons 1267 ref 1269 ref nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp subst appThm 1250 ref refl 1324 def appThm sym 1322 ref 1242 ref refl 1325 def 1277 remove 960 ref appTerm betaConv appThm 1232 ref refl 1326 def 1284 remove 960 ref appTerm betaConv appThm appThm 1290 remove 960 ref appTerm betaConv appThm appThm 1324 remove appThm sym "x" 1203 ref var 1327 def 98 ref 186 remove constTerm 1328 def "a" 3 ref var 1329 def 98 ref 948 ref constTerm 1330 def "b" 928 ref var 1331 def 1206 remove 1327 ref varTerm appTerm 1215 remove 1329 ref varTerm 1332 def appTerm 1331 ref varTerm 1333 def appTerm 1334 def appTerm absTerm appTerm absTerm appTerm absTerm 1335 def 1224 ref appTerm 1336 def betaConv 336 remove "B" 930 remove cons nil cons cons 92 ref cons 1337 def nil 0 ref 1 ref 1 ref 529 ref 4 ref cons opType 1338 def 4 ref cons opType constTerm "x" 529 ref var 1339 def 99 remove 534 remove 98 ref 158 remove constTerm 144 remove 28 ref 1 ref 529 remove 1338 remove nil cons cons opType constTerm 1339 remove varTerm appTerm 536 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm axiom subst nil 161 ref 0 remove 1271 ref constTerm 1335 ref appTerm nil cons cons 162 ref 1336 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp "A" 1208 remove cons nil cons "P" 1204 ref var 1335 remove nil cons cons 1327 remove 1224 ref nil cons cons nil cons cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1328 remove 1329 ref 1330 ref 1331 ref 1225 ref 1334 ref appTerm absTerm appTerm absTerm 1340 def appTerm 1341 def nil cons cons 162 ref 1231 ref 1242 ref 1276 remove appTerm 1232 ref 1283 remove appTerm appTerm 1289 remove appTerm appTerm 1250 remove appTerm 1342 def nil cons 1343 def cons nil cons 1344 def cons nil cons cons 224 ref subst proveHyp nil 329 ref 1002 ref 163 ref 1340 ref 1004 ref appTerm 1345 def appTerm 1342 ref appTerm 1346 def absTerm nil cons cons nil cons nil cons cons 339 ref subst 1002 ref nil 11 ref 1346 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 1345 ref nil cons 1347 def cons 1344 ref cons nil cons cons 1348 def 179 ref subst 1348 remove 237 ref subst 1345 ref betaConv 1345 remove assume eqMp nil 161 ref 1330 remove 1331 ref 1225 ref 1216 remove 1333 ref appTerm appTerm absTerm 1349 def appTerm 1350 def nil cons cons 1344 ref cons nil cons cons 224 ref subst proveHyp nil 937 ref 1238 ref 163 ref 1349 ref 1239 ref appTerm 1351 def appTerm 1342 ref appTerm 1352 def absTerm nil cons cons nil cons nil cons cons 947 ref subst 1238 ref nil 11 ref 1352 remove nil cons cons nil cons nil cons cons 196 ref subst nil 161 ref 1351 ref nil cons 1353 def cons 1344 ref cons nil cons cons 1354 def 179 ref subst 1354 remove 237 ref subst 1351 ref betaConv 1351 remove assume eqMp nil 161 ref 1225 remove 1240 ref appTerm 1355 def nil cons 1356 def cons 1344 remove cons nil cons cons 1357 def 224 ref subst proveHyp 1357 ref 179 ref subst 1357 remove 237 ref subst 1322 ref 1325 ref 1272 ref refl 1273 remove 324 ref refl 1358 def 1002 ref 949 ref refl 1359 def 1238 ref 1274 remove refl nil 11 ref 1275 ref nil cons cons nil cons nil cons cons 338 remove "t" 93 ref var varTerm refl 1360 def subst subst appThm absThm appThm absThm appThm absThm appThm 1355 remove assume 1361 def appThm 1238 ref 29 ref 1272 ref "_29309" 1204 ref var 1362 def 324 ref 1002 ref 949 ref 1238 ref 29 ref 1362 remove varTerm 1240 ref appTerm appTerm 1275 ref appTerm absTerm appTerm absTerm appTerm absTerm 1363 def appTerm 1364 def 1240 ref appTerm appTerm 1275 ref appTerm absTerm 1365 def 1239 ref appTerm 1366 def betaConv 1002 ref 949 ref 1365 ref appTerm 1367 def absTerm 1368 def 1004 ref appTerm 1369 def betaConv 1363 ref 1364 remove appTerm 1370 def betaConv 1363 ref "_29307" 1203 ref var 1371 def 68 ref 1272 remove "fn" 1204 ref var 1372 def 324 ref 1329 ref 949 ref 1331 ref 29 ref 1372 remove varTerm 1334 ref appTerm appTerm 1332 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1373 def 1371 remove varTerm appTerm appTerm absTerm 1374 def appTerm betaConv sym nil 329 ref 1002 ref 949 ref 1238 ref 29 ref 1374 ref 1240 ref appTerm 1375 def appTerm 1275 ref appTerm 1376 def absTerm 1377 def appTerm 1378 def absTerm nil cons cons nil cons nil cons cons 339 ref subst 1002 ref nil 11 ref 1378 remove nil cons cons nil cons nil cons cons 196 ref subst nil 937 ref 1377 remove nil cons cons nil cons nil cons cons 947 ref subst 1238 ref nil 11 ref 1376 remove nil cons cons nil cons nil cons cons 196 ref subst 1375 remove betaConv 29 ref "_29304" 928 ref var 1379 def 1275 ref absTerm 1239 ref appTerm 1380 def appTerm refl 1379 ref 68 ref 1373 ref 1240 ref appTerm 1381 def appTerm 1382 def absTerm 1383 def 1280 ref "fn" 1279 remove var 1384 def 324 ref 1329 ref 949 ref 1331 ref 940 remove 1384 remove varTerm 1334 remove appTerm appTerm 1333 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1385 def 1240 ref appTerm 1386 def appTerm betaConv appThm 204 ref 1380 remove betaConv appThm 1382 remove refl appThm trans 28 remove 1 ref 936 remove 948 remove nil cons cons opType constTerm 1387 def "_29303" 3 ref var 1388 def 1379 remove 68 ref 1388 remove varTerm appTerm absTerm absTerm 1389 def 1004 ref appTerm 1390 def appTerm refl 1389 ref 1381 ref appTerm betaConv appThm 1387 remove refl 1390 remove betaConv appThm 1383 remove refl appThm trans 1389 remove refl nil 1331 remove 1239 ref nil cons 1391 def cons 1329 remove 1004 ref nil cons 1392 def cons nil cons cons nil cons cons 1393 def 1337 ref 740 remove subst subst 1394 def appThm eqMp 1393 remove 1337 remove 762 remove subst subst 1395 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 1205 remove cons nil cons 1396 def "P" 1271 ref var 1363 ref nil cons 1397 def cons "x" 1204 remove var 1374 remove nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp nil 161 ref 98 ref 1 ref 1271 ref 4 ref cons opType constTerm 1363 remove appTerm nil cons cons 162 ref 1370 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp nil "p" 1271 remove var 1397 remove cons nil cons nil cons cons 1396 remove 92 ref cons 738 ref subst subst eqMp eqMp nil 161 ref 324 ref 1368 ref appTerm nil cons cons 162 ref 1369 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 1368 remove nil cons cons 382 ref 1392 remove cons nil cons 1398 def cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1367 remove nil cons cons 162 ref 1366 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 946 ref 937 ref 1365 remove nil cons cons 1267 ref 1391 remove cons nil cons 1399 def cons nil cons cons 244 ref subst eqMp eqMp trans appThm 1326 remove 1280 remove refl 1281 remove 1358 ref 1002 ref 1359 ref 1238 ref 1282 remove refl 1239 ref refl appThm absThm appThm absThm appThm absThm appThm 1361 ref appThm 1395 ref sym trans appThm appThm 1236 ref refl 1400 def 1237 ref 1358 ref 1002 ref 1359 ref 1238 ref 1241 ref refl 1401 def nil "t" 1227 ref var 1402 def 1246 ref nil cons 1403 def cons nil cons nil cons cons "A" 1228 remove cons nil cons 92 ref cons 1404 def 1360 remove subst 1405 def subst 1406 def appThm absThm appThm absThm appThm absThm appThm 1361 ref appThm 1238 ref 1231 ref 1236 ref "_29333" 1233 ref var 1407 def 324 ref 1002 ref 949 ref 1238 ref 1231 ref 1407 remove varTerm 1240 ref appTerm appTerm 1246 ref appTerm absTerm appTerm absTerm appTerm absTerm 1408 def appTerm 1409 def 1240 ref appTerm appTerm 1246 ref appTerm absTerm 1410 def 1239 ref appTerm 1411 def betaConv 1002 ref 949 ref 1410 ref appTerm 1412 def absTerm 1413 def 1004 ref appTerm 1414 def betaConv 1408 ref 1409 remove appTerm 1415 def betaConv 1408 ref "_29331" 1203 ref var 1416 def 1245 ref 959 ref 1385 ref 1416 remove varTerm appTerm 1417 def appTerm appTerm 1417 remove appTerm absTerm 1418 def appTerm betaConv sym nil 329 ref 1002 ref 949 ref 1238 ref 1231 ref 1418 ref 1240 ref appTerm 1419 def appTerm 1246 ref appTerm 1420 def absTerm 1421 def appTerm 1422 def absTerm nil cons cons nil cons nil cons cons 339 ref subst 1002 ref nil 11 ref 1422 remove nil cons cons nil cons nil cons cons 196 ref subst nil 937 ref 1421 remove nil cons cons nil cons nil cons cons 947 ref subst 1238 ref nil 11 ref 1420 remove nil cons cons nil cons nil cons cons 196 ref subst 1419 remove betaConv 1231 ref "_29328" 928 ref var 1423 def 1245 ref 959 ref 1423 remove varTerm 1424 def appTerm appTerm 1424 remove appTerm absTerm 1425 def 1239 ref appTerm 1426 def appTerm refl 1425 ref 1386 ref appTerm betaConv appThm 1322 ref 1426 remove betaConv appThm 1245 ref 959 ref 1386 ref appTerm appTerm 1386 ref appTerm 1427 def refl appThm trans 1425 remove refl 1395 ref appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 1235 remove cons nil cons 1428 def "P" 1234 ref var 1429 def 1408 ref nil cons 1430 def cons "x" 1233 ref var 1431 def 1418 remove nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp nil 161 ref 98 remove 1 ref 1234 ref 4 remove cons opType constTerm 1432 def 1408 remove appTerm nil cons cons 162 ref 1415 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp nil "p" 1234 remove var 1433 def 1430 remove cons nil cons nil cons cons 1428 ref 92 remove cons 738 remove subst 1434 def subst eqMp eqMp nil 161 ref 324 ref 1413 ref appTerm nil cons cons 162 ref 1414 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 1413 remove nil cons cons 1398 ref cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1412 remove nil cons cons 162 ref 1411 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 946 ref 937 ref 1410 remove nil cons cons 1399 ref cons nil cons cons 244 ref subst eqMp eqMp trans appThm appThm 1400 remove 1237 ref 1358 remove 1002 ref 1359 remove 1238 ref 1401 remove nil 1402 remove 1249 ref nil cons cons nil cons nil cons cons 1405 remove subst appThm absThm appThm absThm appThm absThm appThm 1361 remove appThm 1238 ref 1231 ref 1236 ref "_29345" 1233 remove var 1435 def 324 ref 1002 ref 949 ref 1238 ref 1231 ref 1435 remove varTerm 1240 ref appTerm appTerm 1249 ref appTerm absTerm appTerm absTerm appTerm absTerm 1436 def appTerm 1437 def 1240 ref appTerm appTerm 1249 ref appTerm absTerm 1438 def 1239 ref appTerm 1439 def betaConv 1002 ref 949 ref 1438 ref appTerm 1440 def absTerm 1441 def 1004 ref appTerm 1442 def betaConv 1436 ref 1437 remove appTerm 1443 def betaConv 1436 ref "_29343" 1203 remove var 1444 def 1242 ref 1373 remove 1444 remove varTerm 1445 def appTerm appTerm 1245 ref 959 ref 1385 remove 1445 remove appTerm 1446 def appTerm appTerm 1446 ref appTerm appTerm 1232 ref 1446 remove appTerm appTerm absTerm 1447 def appTerm betaConv sym nil 329 ref 1002 ref 949 ref 1238 ref 1231 ref 1447 ref 1240 remove appTerm 1448 def appTerm 1249 ref appTerm 1449 def absTerm 1450 def appTerm 1451 def absTerm nil cons cons nil cons nil cons cons 339 remove subst 1002 ref nil 11 ref 1451 remove nil cons cons nil cons nil cons cons 196 ref subst nil 937 ref 1450 remove nil cons cons nil cons nil cons cons 947 remove subst 1238 ref nil 11 ref 1449 remove nil cons cons nil cons nil cons cons 196 remove subst 1448 remove betaConv 1231 ref "_29340" 928 remove var 1452 def 1243 remove 1245 remove 959 remove 1452 ref varTerm 1453 def appTerm appTerm 1453 ref appTerm 1454 def appTerm 1232 ref 1453 remove appTerm 1455 def appTerm absTerm 1239 ref appTerm 1456 def appTerm refl 1452 ref 1242 ref 1381 ref appTerm 1457 def 1454 ref appTerm 1455 ref appTerm absTerm 1458 def 1386 ref appTerm betaConv appThm 1322 ref 1456 remove betaConv appThm 1457 remove 1427 remove appTerm 1232 ref 1386 remove appTerm appTerm refl appThm trans 1256 ref "_29339" 3 ref var 1459 def 1452 remove 1242 ref 1459 remove varTerm appTerm 1454 remove appTerm 1455 remove appTerm absTerm absTerm 1460 def 1004 ref appTerm 1461 def appTerm refl 1460 ref 1381 remove appTerm betaConv appThm 1256 remove refl 1461 remove betaConv appThm 1458 remove refl appThm trans 1460 remove refl 1394 remove appThm eqMp 1395 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 1428 remove 1429 remove 1436 ref nil cons 1462 def cons 1431 remove 1447 remove nil cons cons nil cons cons nil cons cons 355 ref subst proveHyp nil 161 ref 1432 remove 1436 remove appTerm nil cons cons 162 ref 1443 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp nil 1433 remove 1462 remove cons nil cons nil cons cons 1434 remove subst eqMp eqMp nil 161 ref 324 ref 1441 ref appTerm nil cons cons 162 ref 1442 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 1441 remove nil cons cons 1398 ref cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1440 remove nil cons cons 162 ref 1439 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 946 ref 937 ref 1438 remove nil cons cons 1399 remove cons nil cons cons 244 ref subst eqMp eqMp trans appThm sym nil 161 ref 29 ref 1004 ref appTerm 1463 def 870 ref appTerm 1464 def nil cons 1465 def cons 162 ref 1231 ref 1242 ref 1275 remove appTerm 1248 ref appTerm 1246 ref appTerm appTerm 1249 remove appTerm nil cons 1466 def cons nil cons 1467 def cons nil cons cons 1468 def 179 ref subst 1468 remove 237 ref subst 29 ref "_29349" 3 ref var 1469 def 1231 ref 1242 ref 68 ref 1469 remove varTerm 1470 def appTerm appTerm 1248 ref appTerm 1246 ref appTerm appTerm 1242 ref 1470 remove appTerm 1246 ref appTerm 1248 ref appTerm appTerm absTerm 1471 def 1004 ref appTerm 1472 def appTerm refl 1473 def 1471 ref 870 ref appTerm betaConv appThm 204 remove 1472 remove betaConv appThm 1474 def 1231 ref 1242 ref 883 remove appTerm 1248 ref appTerm 1246 ref appTerm appTerm 1242 ref 870 ref appTerm 1246 ref appTerm 1248 ref appTerm appTerm refl appThm trans 1471 remove refl 1475 def 1464 remove assume appThm eqMp sym 1322 ref 1325 ref 884 remove appThm 1248 ref refl 1476 def appThm 1406 ref appThm nil "t2" 1227 ref var 1477 def 1403 ref cons "t1" 1227 ref var 1478 def 1248 ref nil cons 1479 def cons nil cons cons nil cons cons 1480 def 1404 ref "t2" 93 ref var 1481 def 527 ref 990 remove 1 ref 3 ref 1 remove 93 ref 1303 remove nil cons cons opType nil cons cons opType constTerm 1482 def 37 ref appTerm "t1" 93 remove var 1483 def varTerm 1484 def appTerm 1481 ref varTerm 1485 def appTerm appTerm 1484 ref appTerm absTerm 1486 def 1485 ref appTerm 1487 def betaConv 1483 ref 146 ref 1486 ref appTerm 1488 def absTerm 1489 def 1484 ref appTerm 1490 def betaConv nil 146 ref 1489 ref appTerm 1491 def axiom nil 161 ref 1491 remove nil cons cons 162 ref 1490 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 349 ref 228 ref 1489 remove nil cons cons 232 ref 1484 ref nil cons cons nil cons 1492 def cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1488 remove nil cons cons 162 ref 1487 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 349 ref 228 ref 1486 remove nil cons cons 232 remove 1485 ref nil cons cons nil cons 1493 def cons nil cons cons 244 ref subst eqMp eqMp subst 1494 def subst trans appThm nil 1477 remove 1479 ref cons 1478 remove 1403 ref cons nil cons cons nil cons cons 1495 def 1404 ref 1481 remove 527 remove 1482 remove 870 ref appTerm 1484 ref appTerm 1485 ref appTerm appTerm 1485 ref appTerm absTerm 1496 def 1485 remove appTerm 1497 def betaConv 1483 remove 146 ref 1496 ref appTerm 1498 def absTerm 1499 def 1484 remove appTerm 1500 def betaConv nil 146 remove 1499 ref appTerm 1501 def axiom nil 161 ref 1501 remove nil cons cons 162 ref 1500 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 349 ref 228 ref 1499 remove nil cons cons 1492 remove cons nil cons cons 244 ref subst eqMp eqMp nil 161 ref 1498 remove nil cons cons 162 ref 1497 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 349 remove 228 remove 1496 remove nil cons cons 1493 remove cons nil cons cons 244 ref subst eqMp eqMp subst 1502 def subst appThm nil "x" 1227 remove var 1503 def 1479 remove cons nil cons nil cons cons 1404 remove 921 remove subst 1504 def subst trans sym 195 ref eqMp eqMp eqMp nil 201 ref 1465 ref cons 202 ref 1466 ref cons nil cons 1505 def cons nil cons cons 216 ref subst deductAntisym eqMp nil 161 ref 1463 remove 37 ref appTerm 1506 def nil cons 1507 def cons 1467 remove cons nil cons cons 1508 def 179 remove subst 1508 remove 237 remove subst 1473 remove "_29347" 3 ref var 1509 def 1231 ref 1242 ref 68 ref 1509 remove varTerm 1510 def appTerm appTerm 1248 ref appTerm 1246 ref appTerm appTerm 1242 ref 1510 remove appTerm 1246 ref appTerm 1248 ref appTerm appTerm absTerm 37 ref appTerm betaConv appThm 1474 remove 1231 ref 1242 ref 68 remove 37 ref appTerm 1511 def appTerm 1248 ref appTerm 1246 ref appTerm appTerm 1242 remove 37 remove appTerm 1246 remove appTerm 1248 remove appTerm appTerm refl appThm trans 1475 remove 1506 remove assume appThm eqMp sym 1322 remove 1325 remove nil 29 ref 1511 remove appTerm 870 ref appTerm axiom appThm 1476 remove appThm 1406 remove appThm 1480 remove 1502 remove subst trans appThm 1495 remove 1494 remove subst appThm nil 1503 remove 1403 remove cons nil cons nil cons cons 1504 remove subst trans sym 195 remove eqMp eqMp eqMp nil 201 ref 1507 remove cons 1512 def 1505 remove cons nil cons cons 216 ref subst deductAntisym eqMp 11 remove "Data.Bool.\\/" const 26 remove constTerm 1513 def 194 remove appTerm 193 remove 870 remove appTerm appTerm absTerm 1514 def 1004 remove appTerm 1515 def betaConv nil 324 ref 1514 ref appTerm 1516 def axiom nil 161 ref 1516 remove nil cons cons 162 ref 1515 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 1514 remove nil cons cons 1398 remove cons nil cons cons 244 ref subst eqMp eqMp nil 1512 remove 202 ref 1465 remove cons "R" 3 ref var 1517 def 1466 remove cons nil cons cons cons nil cons cons nil 161 ref 163 ref 207 ref appTerm 1518 def 1517 remove varTerm 1519 def appTerm 1520 def nil cons cons 162 ref 1519 ref nil cons 1521 def cons nil cons cons nil cons cons 224 ref subst nil 161 ref 878 ref 1519 ref appTerm nil cons cons 162 ref 163 ref 1520 remove appTerm 1519 ref appTerm nil cons cons nil cons cons nil cons cons 224 ref subst "r" 3 remove var 1522 def 163 ref 878 remove 1522 ref varTerm 1523 def appTerm appTerm 1524 def 163 ref 1518 remove 1523 ref appTerm appTerm 1523 ref appTerm appTerm absTerm 1525 def 1519 remove appTerm 1526 def betaConv 29 remove 1513 ref 205 ref appTerm 1527 def 207 ref appTerm 1528 def appTerm refl 162 ref 324 ref 1522 ref 1524 remove 163 ref 620 remove 1523 ref appTerm appTerm 1523 ref appTerm 1529 def appTerm absTerm appTerm absTerm 207 remove appTerm betaConv appThm 187 remove 1527 remove appTerm refl 161 ref 162 ref 324 ref 1522 remove 163 ref 165 remove 1523 remove appTerm appTerm 1529 remove appTerm absTerm appTerm absTerm absTerm 1530 def 205 remove appTerm betaConv appThm nil 176 remove 1513 remove appTerm 1530 remove appTerm axiom 214 remove appThm eqMp 210 remove appThm eqMp 1528 remove assume eqMp nil 161 ref 324 ref 1525 ref appTerm nil cons cons 162 ref 1526 remove nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 ref 329 ref 1525 remove nil cons cons 382 ref 1521 remove cons nil cons cons nil cons cons 244 remove subst eqMp eqMp eqMp eqMp subst proveHyp proveHyp proveHyp eqMp eqMp nil 201 ref 1356 remove cons 202 ref 1343 remove cons nil cons 1531 def cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp nil 201 ref 1353 remove cons 1531 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp nil 161 ref 949 ref 1267 remove 163 ref 1349 ref 1269 remove appTerm appTerm 1342 ref appTerm absTerm appTerm nil cons cons 162 ref 163 ref 1350 remove appTerm 1342 ref appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 946 remove 937 remove 1349 remove nil cons cons 1531 ref cons nil cons cons 383 ref subst eqMp eqMp eqMp nil 201 ref 1347 remove cons 1531 ref cons nil cons cons 216 ref subst deductAntisym eqMp eqMp absThm eqMp nil 161 ref 324 ref 382 ref 163 ref 1340 ref 382 remove varTerm appTerm appTerm 1342 ref appTerm absTerm appTerm nil cons cons 162 ref 163 ref 1341 remove appTerm 1342 remove appTerm nil cons cons nil cons cons nil cons cons 224 ref subst proveHyp 337 remove 329 remove 1340 remove nil cons cons 1531 remove cons nil cons cons 383 ref subst eqMp eqMp eqMp eqMp eqMp absThm eqMp eqMp 1259 ref 1306 ref 1253 remove nil cons cons 1307 ref 1232 remove nil cons cons nil cons cons nil cons cons 355 remove subst proveHyp eqMp nil 201 ref 1319 remove cons 202 remove 1312 remove cons nil cons 1532 def cons nil cons cons 216 ref subst deductAntisym eqMp eqMp eqMp nil 201 remove 1316 remove cons 1532 ref cons nil cons cons 216 remove subst deductAntisym eqMp eqMp absThm eqMp nil 161 remove 1294 remove 1307 ref 163 ref 1309 ref 1307 remove varTerm appTerm appTerm 1311 ref appTerm absTerm appTerm nil cons cons 162 remove 163 remove 1310 remove appTerm 1311 remove appTerm nil cons cons nil cons cons nil cons cons 224 remove subst proveHyp 1259 remove 1306 remove 1309 remove nil cons cons 1532 remove cons nil cons cons 383 remove subst eqMp eqMp eqMp eqMp defineConstList 1533 def pop 1534 def pop 1533 remove nil 949 ref 953 remove 1231 remove 1534 remove hdTl pop 1229 remove constTerm 1535 def 960 remove appTerm appTerm 1236 remove 1237 remove 324 remove 1002 remove 949 remove 1238 remove 1241 remove 1247 remove 1535 remove 1239 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1224 remove appTerm appTerm absTerm appTerm thm