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