path: "vendor/opentheory/data/theories/word-bits-thm/word-bits-thm.art"
6 version "Data.Bool.!" const 0 def "->" typeOp 1 def 1 ref "Data.Word.word" typeOp nil opType 2 def "bool" typeOp nil opType 3 def nil cons 4 def cons opType 5 def 4 ref cons opType constTerm 6 def refl 7 def "w" 2 ref var 8 def nil "l" "Data.List.list" typeOp 9 def 4 ref opType 10 def var 11 def "Data.Word.Bits.fromWord" const 1 ref 2 ref 10 ref nil cons 12 def cons opType constTerm 13 def 8 ref varTerm 14 def appTerm 15 def nil cons cons 16 def nil cons 17 def nil cons cons 18 def 11 ref "=" const 19 def 1 ref 3 ref 1 ref 3 ref 4 ref cons opType 20 def nil cons cons opType 21 def constTerm 22 def "Data.Word.Bits.normal" const 1 ref 10 ref 4 ref cons opType 23 def constTerm 24 def 11 ref varTerm 25 def appTerm appTerm 26 def 19 ref 1 ref "Number.Natural.natural" typeOp nil opType 27 def 1 ref 27 ref 4 ref cons opType 28 def nil cons 29 def cons opType 30 def constTerm 31 def "Data.List.length" const 32 def 1 ref 10 ref 27 ref nil cons 33 def cons opType 34 def constTerm 35 def 25 ref appTerm 36 def appTerm "Data.Word.width" const 27 ref constTerm 37 def appTerm 38 def appTerm absTerm 39 def 25 ref appTerm 40 def betaConv nil 0 ref 1 ref 23 ref 4 ref cons opType constTerm 41 def 39 ref appTerm 42 def axiom nil "p" 3 ref var 43 def 42 remove nil cons cons "q" 3 ref var 44 def 40 remove nil cons cons nil cons cons nil cons cons 22 ref "Data.Bool.==>" const 21 ref constTerm 45 def 43 ref varTerm 46 def appTerm 47 def 44 ref varTerm 48 def appTerm 49 def appTerm refl 43 ref 44 ref 22 ref "Data.Bool./\\" const 21 ref constTerm 50 def 46 ref appTerm 51 def 48 ref appTerm 52 def appTerm 53 def 46 ref appTerm absTerm 54 def absTerm 55 def 46 ref appTerm betaConv 48 ref refl 56 def appThm 54 remove 48 ref appTerm betaConv trans appThm nil 19 ref 1 ref 21 ref 1 ref 21 ref 4 ref cons opType 57 def nil cons cons opType constTerm 58 def 45 ref appTerm 55 remove appTerm axiom 46 ref refl 59 def appThm 56 ref appThm eqMp 60 def sym 61 def 53 remove refl 44 ref 19 ref 1 ref 57 ref 1 ref 57 remove 4 ref cons opType nil cons cons opType constTerm 62 def "f" 21 ref var 63 def 63 ref varTerm 64 def 46 ref appTerm 48 ref appTerm absTerm 65 def appTerm 63 ref 64 ref "Data.Bool.T" const 3 ref constTerm 66 def appTerm 66 ref appTerm absTerm 67 def appTerm absTerm 68 def 48 ref appTerm betaConv appThm 19 ref 1 ref 20 ref 1 ref 20 ref 4 ref cons opType 69 def nil cons cons opType constTerm 70 def 51 ref appTerm refl 43 ref 68 remove absTerm 71 def 46 ref appTerm betaConv appThm nil 58 ref 50 ref appTerm 71 ref appTerm axiom 72 def 59 remove appThm eqMp 56 ref appThm eqMp 73 def sym 63 ref 64 ref refl nil "t" 3 ref var 74 def 46 ref nil cons 75 def cons nil cons nil cons cons 22 ref 74 ref varTerm 76 def appTerm 77 def 66 ref appTerm 78 def assume sym nil 66 ref axiom 79 def eqMp 76 ref assume 79 ref deductAntisym deductAntisym 80 def subst 46 ref assume 81 def eqMp appThm nil 74 ref 48 ref nil cons 82 def cons nil cons nil cons cons 83 def 80 ref subst 48 ref assume 84 def eqMp appThm absThm eqMp 85 def nil "P" 3 ref var 86 def 75 ref cons "Q" 3 ref var 87 def 82 ref cons nil cons 88 def cons nil cons cons 22 ref refl 89 def 63 ref 64 remove 86 ref varTerm 90 def appTerm 91 def 87 ref varTerm 92 def appTerm absTerm 93 def 43 ref 44 ref 46 ref absTerm absTerm 94 def appTerm betaConv 94 ref 90 ref appTerm betaConv 92 ref refl 95 def appThm 44 ref 90 ref absTerm 92 ref appTerm betaConv trans trans appThm 67 ref 94 ref appTerm betaConv 94 ref 66 ref appTerm betaConv 66 ref refl 96 def appThm 44 ref 66 ref absTerm 66 ref appTerm betaConv trans trans appThm 22 ref 50 ref 90 ref appTerm 97 def 92 ref appTerm 98 def appTerm refl 44 ref 62 remove 63 remove 91 remove 48 ref appTerm absTerm appTerm 67 ref appTerm absTerm 92 ref appTerm betaConv appThm 70 ref 97 remove appTerm refl 71 remove 90 ref appTerm betaConv appThm 72 remove 90 ref refl 99 def appThm eqMp 95 ref appThm eqMp 98 remove assume eqMp 100 def 94 remove refl appThm eqMp sym 79 ref eqMp 101 def subst 102 def deductAntisym eqMp 60 remove 49 ref assume eqMp sym 81 ref eqMp 89 ref 65 remove 43 ref 44 ref 48 ref absTerm 103 def absTerm 104 def appTerm betaConv 104 ref 46 ref appTerm betaConv 56 remove appThm 103 ref 48 ref appTerm betaConv trans trans appThm 67 remove 104 ref appTerm betaConv 104 ref 66 ref appTerm betaConv 96 remove appThm 103 ref 66 ref appTerm betaConv trans trans 105 def appThm 73 remove 52 ref assume eqMp 104 ref refl 106 def appThm eqMp sym 79 ref eqMp 107 def proveHyp deductAntisym 108 def subst proveHyp "A" 12 ref cons nil cons 109 def "P" 23 ref var 110 def 39 remove nil cons cons "x" 10 ref var 111 def 25 ref nil cons 112 def cons nil cons 113 def cons nil cons cons nil 43 ref 0 ref 1 ref 1 ref "A" varType 114 def 4 ref cons opType 115 def 4 ref cons opType 116 def constTerm 117 def "P" 115 ref var 118 def varTerm 119 def appTerm 120 def nil cons 121 def cons 44 ref 119 ref "x" 114 ref var 122 def varTerm 123 def appTerm 124 def nil cons 125 def cons nil cons cons nil cons cons 126 def 61 ref subst 126 remove 107 remove 85 remove deductAntisym 127 def subst 22 ref 124 ref appTerm refl 122 ref 66 ref absTerm 128 def 123 ref appTerm betaConv appThm "p" 115 ref var 129 def 19 ref 1 ref 115 ref 116 ref nil cons cons opType constTerm 129 ref varTerm 130 def appTerm 128 remove appTerm absTerm 131 def 119 ref appTerm betaConv 132 def nil 19 ref 1 ref 116 ref 1 ref 116 ref 4 ref cons opType 133 def nil cons cons opType constTerm 134 def 117 ref appTerm 131 remove appTerm axiom 119 ref refl 135 def appThm 136 def 120 ref assume eqMp eqMp 123 ref refl 137 def appThm eqMp sym 79 ref eqMp eqMp nil 86 ref 121 remove cons 87 ref 125 ref cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp 138 def subst eqMp eqMp 139 def subst 31 ref refl 140 def 35 ref refl 141 def 8 ref 19 ref 1 ref 10 ref 23 ref nil cons 142 def cons opType 143 def constTerm 144 def 15 ref appTerm "Number.Natural.Bits.toVector" const 1 ref 27 ref 1 ref 27 ref 12 ref cons opType nil cons 145 def cons opType constTerm 146 def "Data.Word.toNatural" const 1 ref 2 ref 33 ref cons opType constTerm 147 def 14 ref appTerm 148 def appTerm 37 ref appTerm appTerm absTerm 149 def 14 ref appTerm 150 def betaConv nil 6 ref 149 ref appTerm 151 def axiom nil 43 ref 151 remove nil cons cons 44 ref 150 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp "A" 2 ref nil cons 152 def cons nil cons 153 def "P" 5 ref var 154 def 149 remove nil cons cons "x" 2 ref var 155 def 14 ref nil cons cons nil cons 156 def cons nil cons cons 138 ref subst eqMp eqMp 157 def appThm nil "k" 27 ref var 158 def 37 ref nil cons 159 def cons 160 def "n" 27 ref var 161 def 148 ref nil cons 162 def cons nil cons cons nil cons cons 163 def 158 ref 31 ref 35 ref 146 ref 161 ref varTerm 164 def appTerm 158 ref varTerm 165 def appTerm 166 def appTerm appTerm 165 ref appTerm absTerm 167 def 165 ref appTerm 168 def betaConv 161 ref 0 ref 1 ref 28 ref 4 ref cons opType 169 def constTerm 170 def 167 ref appTerm 171 def absTerm 172 def 164 ref appTerm 173 def betaConv nil 170 ref 172 ref appTerm 174 def axiom nil 43 ref 174 remove nil cons cons 44 ref 173 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp "A" 33 ref cons 175 def nil cons 176 def "P" 28 remove var 177 def 172 remove nil cons cons "x" 27 ref var 178 def 164 ref nil cons 179 def cons nil cons 180 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 171 remove nil cons cons 44 ref 168 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 167 remove nil cons cons 178 ref 165 ref nil cons 181 def cons nil cons 182 def cons nil cons cons 138 ref subst eqMp eqMp subst trans 183 def appThm 37 ref refl 184 def appThm nil 178 ref 159 ref cons nil cons 185 def nil cons cons 176 ref nil nil cons 186 def cons 187 def nil 74 ref 19 ref 1 ref 114 ref 115 ref nil cons 188 def cons opType constTerm 189 def 123 ref appTerm 190 def 123 ref appTerm nil cons cons nil cons nil cons cons 80 ref subst 137 remove eqMp 191 def subst 192 def subst 193 def trans 194 def trans absThm appThm nil 74 ref 66 ref nil cons 195 def cons nil cons nil cons cons 196 def 153 ref 186 ref cons 197 def 74 ref 22 ref 117 ref 122 ref 76 ref absTerm appTerm appTerm 76 ref appTerm absTerm 198 def 76 ref appTerm 199 def betaConv nil 0 ref 69 remove constTerm 200 def 198 ref appTerm 201 def axiom nil 43 ref 201 remove nil cons cons 44 ref 199 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp "A" 4 ref cons 202 def nil cons 203 def "P" 20 ref var 204 def 198 remove nil cons cons "x" 3 ref var 205 def 76 ref nil cons cons nil cons 206 def cons nil cons cons 138 ref subst eqMp eqMp 207 def subst subst 208 def trans sym 79 ref eqMp nil 6 ref 8 ref 24 remove 15 ref appTerm absTerm appTerm thm nil 11 ref "Data.List.[]" const 209 def 10 ref constTerm 210 def nil cons cons nil cons nil cons cons 11 ref 19 ref 1 ref 2 ref 5 remove nil cons cons opType 211 def constTerm 212 def "Data.Word.Bits.toWord" const 1 ref 10 ref 152 ref cons opType constTerm 213 def 25 ref appTerm 214 def appTerm "Data.Word.fromNatural" const 1 ref 27 ref 152 ref cons opType 215 def constTerm 216 def "Number.Natural.Bits.fromList" const 34 remove constTerm 217 def 25 ref appTerm 218 def appTerm 219 def appTerm absTerm 220 def 25 ref appTerm 221 def betaConv nil 41 ref 220 ref appTerm 222 def axiom nil 43 ref 222 remove nil cons cons 44 ref 221 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 220 remove nil cons cons 113 ref cons nil cons cons 138 ref subst eqMp eqMp 223 def subst 216 ref refl 224 def nil 31 ref 217 ref 210 ref appTerm 225 def appTerm "Number.Natural.zero" const 27 ref constTerm 226 def appTerm axiom 227 def appThm trans 228 def nil 212 ref 213 ref 210 ref appTerm 229 def appTerm 216 ref 226 ref appTerm 230 def appTerm thm 147 ref refl 231 def 228 ref appThm nil 161 ref 226 ref nil cons 232 def cons nil cons nil cons cons 233 def 161 ref 31 ref 147 ref 216 ref 164 ref appTerm appTerm appTerm 234 def "Number.Natural.Bits.bound" const 1 ref 27 ref 1 ref 27 ref 33 ref cons opType 235 def nil cons 236 def cons opType 237 def constTerm 238 def 164 ref appTerm 239 def 37 ref appTerm appTerm absTerm 240 def 164 ref appTerm 241 def betaConv 170 ref refl 242 def 161 ref 140 ref 161 ref 234 remove "Number.Natural.mod" const 237 ref constTerm 243 def 164 ref appTerm 244 def "Data.Word.modulus" const 27 ref constTerm 245 def appTerm appTerm absTerm 246 def 164 ref appTerm 247 def betaConv nil 170 ref 246 ref appTerm 248 def axiom nil 43 ref 248 remove nil cons cons 44 ref 247 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 246 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp 244 ref refl nil 31 ref 245 ref appTerm "Number.Natural.^" const 237 ref constTerm "Number.Natural.bit0" const 235 ref constTerm "Number.Natural.bit1" const 235 ref constTerm 226 ref appTerm 249 def appTerm 250 def appTerm 251 def 37 ref appTerm 252 def appTerm 253 def axiom 254 def appThm trans appThm nil 160 ref nil cons nil cons cons 255 def 158 ref 31 ref 239 ref 165 ref appTerm 256 def appTerm 257 def 244 ref 251 ref 165 ref appTerm 258 def appTerm appTerm absTerm 259 def 165 ref appTerm 260 def betaConv 161 ref 170 ref 259 ref appTerm 261 def absTerm 262 def 164 ref appTerm 263 def betaConv nil 170 ref 262 ref appTerm 264 def axiom nil 43 ref 264 remove nil cons cons 44 ref 263 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 262 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 261 remove nil cons cons 44 ref 260 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 259 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp 265 def subst appThm nil 178 ref 244 remove 252 ref appTerm nil cons cons nil cons nil cons cons 192 ref subst trans absThm appThm 196 ref 187 ref 207 ref subst subst 266 def trans sym 79 ref eqMp 267 def nil 43 ref 170 ref 240 ref appTerm 268 def nil cons cons 44 ref 241 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 240 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp 269 def subst 255 ref 158 ref 31 ref 238 ref 226 ref appTerm 165 ref appTerm appTerm 226 ref appTerm absTerm 270 def 165 ref appTerm 271 def betaConv nil 170 ref 270 ref appTerm 272 def axiom nil 43 ref 272 remove nil cons cons 44 ref 271 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 270 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans trans nil 31 ref 147 ref 229 ref appTerm appTerm 226 ref appTerm thm 7 ref 8 ref 212 ref refl 273 def 18 remove 223 ref subst 224 ref 217 ref refl 274 def 157 ref appThm 275 def 163 ref 158 ref 31 ref 217 ref 166 ref appTerm appTerm 256 ref appTerm absTerm 276 def 165 ref appTerm 277 def betaConv 161 ref 170 ref 276 ref appTerm 278 def absTerm 279 def 164 ref appTerm 280 def betaConv nil 170 ref 279 ref appTerm 281 def axiom nil 43 ref 281 remove nil cons cons 44 ref 280 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 279 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 278 remove nil cons cons 44 ref 277 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 276 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp 282 def subst 283 def 163 ref 265 remove subst 243 ref 148 ref appTerm refl 31 ref 252 remove appTerm 245 ref appTerm assume sym 253 remove assume sym deductAntisym 254 remove eqMp 284 def appThm nil 156 ref nil cons cons 285 def 155 ref 31 ref 243 remove 147 ref 155 ref varTerm 286 def appTerm 287 def appTerm 245 ref appTerm appTerm 287 ref appTerm absTerm 288 def 286 ref appTerm 289 def betaConv nil 6 ref 288 ref appTerm 290 def axiom nil 43 ref 290 remove nil cons cons 44 ref 289 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 288 remove nil cons cons 155 ref 286 ref nil cons cons nil cons 291 def cons nil cons cons 138 ref subst eqMp eqMp subst trans trans 292 def trans trans 293 def appThm 285 ref 155 ref 212 ref 216 ref 287 ref appTerm 294 def appTerm 286 ref appTerm 295 def absTerm 296 def 286 ref appTerm 297 def betaConv nil 6 ref 296 ref appTerm 298 def axiom 299 def nil 43 ref 298 remove nil cons cons 44 ref 297 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 296 remove nil cons cons 291 ref cons nil cons cons 138 ref subst eqMp eqMp 300 def subst trans trans appThm 14 ref refl appThm 285 ref 197 ref 191 ref subst 301 def subst trans absThm appThm 208 ref trans sym 79 ref eqMp 302 def nil 6 ref 8 ref 212 ref 213 ref 15 ref appTerm 303 def appTerm 14 ref appTerm 304 def absTerm appTerm thm 7 ref 8 ref 194 remove absThm appThm 208 ref trans sym 79 ref eqMp nil 6 ref 8 ref 31 ref 35 ref 15 ref appTerm 305 def appTerm 37 ref appTerm absTerm appTerm thm 7 ref 8 ref 163 remove 158 ref 22 ref "Number.Natural.<=" const 30 ref constTerm 306 def "Number.Natural.Bits.width" const 235 ref constTerm 307 def 164 ref appTerm appTerm 165 ref appTerm 308 def appTerm "Number.Natural.<" const 30 ref constTerm 309 def 164 ref appTerm 310 def 258 remove appTerm appTerm absTerm 311 def 165 ref appTerm 312 def betaConv 161 ref 170 ref 311 ref appTerm 313 def absTerm 314 def 164 ref appTerm 315 def betaConv nil 170 ref 314 ref appTerm 316 def axiom nil 43 ref 316 remove nil cons cons 44 ref 315 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 314 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 313 remove nil cons cons 44 ref 312 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 311 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp subst 309 ref 148 ref appTerm refl 284 remove appThm 285 remove nil 74 ref 309 ref 287 ref appTerm 317 def 245 remove appTerm 318 def nil cons cons nil cons nil cons cons 80 ref subst 155 ref 318 remove absTerm 319 def 286 ref appTerm 320 def betaConv nil 6 ref 319 ref appTerm 321 def axiom nil 43 ref 321 remove nil cons cons 44 ref 320 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 319 remove nil cons cons 291 ref cons nil cons cons 138 ref subst eqMp eqMp eqMp subst trans trans absThm appThm 208 ref trans sym 79 ref eqMp nil 6 ref 8 ref 306 ref 307 ref 148 ref appTerm appTerm 37 ref appTerm absTerm appTerm thm 7 ref 8 ref 140 ref 275 remove 283 remove trans appThm 148 ref refl 322 def appThm 140 ref 292 remove appThm 322 remove appThm nil 178 ref 162 remove cons nil cons nil cons cons 192 ref subst trans 323 def trans absThm appThm 208 ref trans sym 79 ref eqMp nil 6 ref 8 ref 31 ref 217 ref 15 ref appTerm appTerm 148 ref appTerm absTerm appTerm thm 7 ref 8 ref 323 remove absThm appThm 208 remove trans sym 79 ref eqMp nil 6 ref 8 ref 31 ref 238 ref 148 ref appTerm 37 ref appTerm appTerm 148 ref appTerm absTerm appTerm thm 267 remove nil 268 remove thm nil 110 ref 11 ref 26 remove 144 ref 13 ref 214 ref appTerm appTerm 324 def 25 ref appTerm 325 def appTerm 326 def absTerm 327 def nil cons cons nil cons nil cons cons 109 ref 186 ref cons 328 def 22 ref 120 remove appTerm refl 132 remove appThm 136 remove eqMp sym 329 def subst 330 def subst 11 ref nil 74 ref 326 remove nil cons cons nil cons nil cons cons 80 ref subst 89 ref 139 remove appThm 325 ref refl appThm sym nil 43 ref 38 ref nil cons 331 def cons 332 def 44 ref 325 ref nil cons 333 def cons nil cons cons nil cons cons 334 def 61 ref 127 ref 22 ref 46 ref appTerm 48 ref appTerm 335 def assume 336 def 81 remove eqMp eqMp 102 remove deductAntisym eqMp 337 def nil 43 ref 49 remove nil cons 338 def cons 44 ref 45 ref 48 ref appTerm 339 def 46 ref appTerm nil cons 340 def cons nil cons cons nil cons cons 127 ref subst proveHyp 339 ref refl 336 remove appThm sym nil 43 ref 82 ref cons 341 def 44 ref 82 ref cons nil cons cons nil cons cons 342 def 61 ref subst 342 remove 127 ref subst 84 remove eqMp nil 86 ref 82 ref cons 88 remove cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp nil 341 remove 44 ref 75 ref cons nil cons cons nil cons cons 108 ref subst nil 86 ref 338 ref cons 87 ref 340 remove cons nil cons cons nil cons cons 343 def 89 ref 93 remove 104 ref appTerm betaConv 104 remove 90 ref appTerm betaConv 95 ref appThm 103 remove 92 ref appTerm betaConv trans trans appThm 105 remove appThm 100 remove 106 remove appThm eqMp sym 79 ref eqMp subst eqMp 108 ref 343 remove 101 ref subst eqMp deductAntisym deductAntisym 344 def subst 334 ref 61 ref subst 334 remove 127 ref subst nil 8 ref 214 ref nil cons cons nil cons nil cons cons 345 def 157 ref subst 146 ref refl 231 ref 223 ref appThm 346 def nil 161 ref 218 ref nil cons 347 def cons nil cons 348 def nil cons cons 269 ref subst 349 def trans 350 def appThm 184 ref appThm nil 160 ref 348 ref cons 351 def nil cons cons 352 def 158 ref 144 ref 146 ref 256 ref appTerm 165 ref appTerm appTerm 166 ref appTerm absTerm 353 def 165 ref appTerm 354 def betaConv 161 ref 170 ref 353 ref appTerm 355 def absTerm 356 def 164 ref appTerm 357 def betaConv nil 170 ref 356 ref appTerm 358 def axiom nil 43 ref 358 remove nil cons cons 44 ref 357 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 356 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 355 remove nil cons cons 44 ref 354 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 353 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp subst 255 remove 158 ref 144 ref 146 ref 218 ref appTerm 165 ref appTerm appTerm "Data.Bool.cond" const 359 def 1 ref 3 ref 1 ref 10 ref 1 ref 10 ref 12 ref cons opType nil cons 360 def cons opType 361 def nil cons 362 def cons opType constTerm 363 def 306 ref 36 ref appTerm 364 def 165 ref appTerm 365 def appTerm "Data.List.@" const 366 def 361 remove constTerm 367 def 25 ref appTerm 368 def "Data.List.replicate" const 369 def 1 ref 3 ref 145 remove cons opType constTerm "Data.Bool.F" const 3 ref constTerm 370 def appTerm 371 def "Number.Natural.-" const 237 ref constTerm 372 def 165 ref appTerm 36 ref appTerm appTerm appTerm appTerm "Data.List.take" const 373 def 1 ref 27 ref 360 ref cons opType 374 def constTerm 375 def 165 ref appTerm 25 ref appTerm appTerm appTerm absTerm 376 def 165 ref appTerm 377 def betaConv 11 ref 170 ref 376 ref appTerm 378 def absTerm 379 def 25 ref appTerm 380 def betaConv nil 41 ref 379 ref appTerm 381 def axiom nil 43 ref 381 remove nil cons cons 44 ref 380 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 379 remove nil cons cons 113 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 378 remove nil cons cons 44 ref 377 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 376 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans trans trans 382 def 363 ref refl 306 ref refl 383 def 38 ref assume 384 def appThm 184 ref appThm nil 161 ref 159 ref cons 385 def nil cons 386 def nil cons cons 387 def nil 74 ref 306 ref 164 ref appTerm 388 def 164 ref appTerm 389 def nil cons cons nil cons nil cons cons 80 ref subst 161 ref 389 remove absTerm 390 def 164 ref appTerm 391 def betaConv nil 170 ref 390 ref appTerm 392 def axiom nil 43 ref 392 remove nil cons cons 44 ref 391 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 390 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp eqMp subst 393 def trans 394 def appThm 368 ref refl 371 ref refl 372 ref 37 ref appTerm 395 def refl 384 ref appThm 387 remove 161 ref 31 ref 372 remove 164 ref appTerm 164 ref appTerm appTerm 226 ref appTerm absTerm 396 def 164 ref appTerm 397 def betaConv nil 170 ref 396 ref appTerm 398 def axiom nil 43 ref 398 remove nil cons cons 44 ref 397 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 396 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans appThm nil 205 ref 370 ref nil cons 399 def cons nil cons 400 def nil cons cons 401 def 203 ref 186 ref cons 402 def 122 ref 19 ref 1 ref 9 ref 114 ref nil cons 403 def opType 404 def 1 ref 404 ref 4 ref cons opType 405 def nil cons 406 def cons opType constTerm 407 def 369 remove 1 ref 114 ref 1 ref 27 ref 404 ref nil cons 408 def cons opType nil cons cons opType constTerm 123 ref appTerm 409 def 226 ref appTerm appTerm 209 remove 404 ref constTerm 410 def appTerm absTerm 411 def 123 ref appTerm 412 def betaConv nil 117 ref 411 ref appTerm 413 def axiom nil 43 ref 413 remove nil cons cons 44 ref 412 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp "A" 403 ref cons nil cons 414 def 118 ref 411 remove nil cons cons 122 ref 123 ref nil cons cons nil cons 415 def cons nil cons cons 138 ref subst eqMp eqMp subst subst trans appThm 402 ref "l" 404 ref var 416 def 407 ref 366 remove 1 ref 404 ref 1 ref 404 ref 408 ref cons opType nil cons 417 def cons opType constTerm 416 ref varTerm 418 def appTerm 410 ref appTerm appTerm 418 ref appTerm absTerm 419 def 418 ref appTerm 420 def betaConv nil 0 ref 1 ref 405 ref 4 ref cons opType 421 def constTerm 422 def 419 ref appTerm 423 def axiom nil 43 ref 423 remove nil cons cons 44 ref 420 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp "A" 408 remove cons nil cons 424 def "P" 405 ref var 425 def 419 remove nil cons cons "x" 404 ref var 426 def 418 ref nil cons cons nil cons 427 def cons nil cons cons 138 ref subst eqMp eqMp subst trans appThm 375 ref 37 ref appTerm 25 ref appTerm 428 def refl appThm nil "t2" 10 ref var 429 def 428 ref nil cons 430 def cons "t1" 10 ref var 431 def 112 ref cons nil cons cons nil cons cons 328 ref "t2" 114 ref var 432 def 189 ref 359 ref 1 ref 3 ref 1 ref 114 ref 1 ref 114 ref 403 ref cons opType nil cons cons opType nil cons cons opType constTerm 433 def 66 ref appTerm "t1" 114 ref var 434 def varTerm 435 def appTerm 432 ref varTerm 436 def appTerm appTerm 435 ref appTerm absTerm 437 def 436 ref appTerm 438 def betaConv 434 ref 117 ref 437 ref appTerm 439 def absTerm 440 def 435 ref appTerm 441 def betaConv nil 117 ref 440 ref appTerm 442 def axiom nil 43 ref 442 remove nil cons cons 44 ref 441 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 440 remove nil cons cons 122 ref 435 ref nil cons cons nil cons 443 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 439 remove nil cons cons 44 ref 438 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 437 remove nil cons cons 122 ref 436 ref nil cons cons nil cons 444 def cons nil cons cons 138 ref subst eqMp eqMp 445 def subst subst trans trans eqMp nil 86 ref 331 ref cons 446 def 87 ref 333 ref cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp nil 43 ref 45 ref 38 ref appTerm 325 ref appTerm nil cons cons 44 ref 45 ref 325 ref appTerm 38 ref appTerm nil cons cons nil cons cons nil cons cons 127 ref subst proveHyp nil 43 ref 333 ref cons 44 ref 331 ref cons nil cons cons nil cons cons 447 def 61 ref subst 447 remove 127 ref subst 140 ref 141 remove 325 remove assume sym appThm appThm 184 ref appThm sym 345 ref 183 ref subst eqMp eqMp nil 86 ref 333 remove cons 87 ref 331 ref cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp eqMp eqMp absThm eqMp nil 41 ref 327 remove appTerm thm nil 110 ref 11 ref 309 ref 147 ref 214 ref appTerm appTerm 251 remove 36 ref appTerm 448 def appTerm 449 def absTerm 450 def nil cons cons nil cons nil cons cons 330 ref subst 11 ref nil 74 ref 449 remove nil cons cons nil cons nil cons cons 80 ref subst 309 ref refl 451 def 350 ref appThm 448 ref refl appThm sym 161 ref 50 ref 306 ref 238 ref 218 ref appTerm 452 def 37 ref appTerm 453 def appTerm 164 ref appTerm appTerm 310 ref 448 ref appTerm appTerm absTerm 454 def 218 ref appTerm betaConv sym 50 ref refl 455 def 352 ref nil 74 ref 306 ref 256 ref appTerm 164 ref appTerm 456 def nil cons cons nil cons nil cons cons 80 ref subst 158 ref 456 remove absTerm 457 def 165 ref appTerm 458 def betaConv 161 ref 170 ref 457 ref appTerm 459 def absTerm 460 def 164 ref appTerm 461 def betaConv nil 170 ref 460 ref appTerm 462 def axiom nil 43 ref 462 remove nil cons cons 44 ref 461 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 460 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 459 remove nil cons cons 44 ref 458 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 457 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp eqMp subst appThm nil 74 ref 309 ref 218 ref appTerm 448 ref appTerm 463 def nil cons cons nil cons nil cons cons 80 ref subst 11 ref 463 remove absTerm 464 def 25 ref appTerm 465 def betaConv nil 41 ref 464 ref appTerm 466 def axiom nil 43 ref 466 remove nil cons cons 44 ref 465 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 464 remove nil cons cons 113 ref cons nil cons cons 138 ref subst eqMp eqMp eqMp appThm 196 ref 74 ref 22 ref 50 ref 66 ref appTerm 76 ref appTerm appTerm 76 ref appTerm absTerm 467 def 76 ref appTerm 468 def betaConv nil 200 ref 467 ref appTerm 469 def axiom nil 43 ref 469 remove nil cons cons 44 ref 468 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 467 remove nil cons cons 206 ref cons nil cons cons 138 ref subst eqMp eqMp 470 def subst 471 def trans sym 79 ref eqMp eqMp 176 ref 177 ref 454 ref nil cons cons 178 ref 347 remove cons nil cons cons nil cons cons 22 ref "Data.Bool.?" const 472 def 116 ref constTerm 473 def 119 ref appTerm 474 def appTerm 475 def refl 129 ref 200 ref 44 ref 45 ref 117 ref 122 ref 45 ref 130 ref 123 ref appTerm 476 def appTerm 48 ref appTerm absTerm appTerm appTerm 48 ref appTerm absTerm appTerm absTerm 477 def 119 remove appTerm betaConv appThm nil 134 remove 473 remove appTerm 477 remove appTerm axiom 135 remove appThm eqMp 478 def sym nil 204 ref 87 ref 45 ref 117 ref 122 ref 45 ref 124 remove appTerm 479 def 92 ref appTerm absTerm 480 def appTerm 481 def appTerm 92 ref appTerm 482 def absTerm nil cons cons nil cons nil cons cons 402 ref 329 ref subst 483 def subst 87 ref nil 74 ref 482 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 481 remove nil cons 484 def cons 485 def 44 ref 92 ref nil cons 486 def cons nil cons 487 def cons nil cons cons 488 def 61 ref subst 488 ref 127 ref subst nil 43 ref 125 remove cons 487 ref cons nil cons cons 108 ref subst 480 ref 123 ref appTerm 489 def betaConv nil 485 ref 44 ref 489 remove nil cons cons nil cons cons nil cons cons 108 ref subst 414 ref 118 ref 480 remove nil cons cons 415 ref cons nil cons cons 138 ref subst eqMp eqMp eqMp eqMp nil 86 ref 484 remove cons 490 def 87 ref 486 ref cons nil cons 491 def cons nil cons cons 101 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 492 def subst proveHyp nil 43 ref 472 remove 169 remove constTerm 493 def 454 remove appTerm nil cons cons 44 ref 309 ref 453 ref appTerm 448 ref appTerm nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp nil "p" 27 ref var 494 def 448 remove nil cons cons "m" 27 ref var 495 def 453 ref nil cons 496 def cons nil cons cons nil cons cons 494 ref 45 ref 493 ref 161 ref 50 ref 306 ref 495 ref varTerm 497 def appTerm 498 def 164 ref appTerm 499 def appTerm 500 def 310 ref 494 ref varTerm 501 def appTerm appTerm 502 def absTerm 503 def appTerm 504 def appTerm 505 def 309 ref 497 ref appTerm 506 def 501 ref appTerm 507 def appTerm 508 def absTerm 509 def 501 ref appTerm 510 def betaConv 495 ref 170 ref 509 ref appTerm 511 def absTerm 512 def 497 ref appTerm 513 def betaConv nil 170 ref 495 ref 170 ref 161 ref 170 ref 494 ref 45 ref 502 ref appTerm 507 ref appTerm absTerm 514 def appTerm 515 def absTerm 516 def appTerm 517 def absTerm 518 def appTerm 519 def axiom nil 43 ref 519 ref nil cons 520 def cons 521 def 44 ref 170 ref 512 ref appTerm nil cons 522 def cons nil cons cons nil cons cons 523 def 108 ref subst proveHyp 523 ref 61 ref subst 523 remove 127 ref subst nil 177 ref 512 remove nil cons cons 524 def nil cons nil cons cons 187 ref 329 ref subst 525 def subst 495 ref nil 74 ref 511 remove nil cons 526 def cons nil cons nil cons cons 80 ref subst nil 177 ref 509 remove nil cons cons 527 def nil cons nil cons cons 525 ref subst 494 ref nil 74 ref 508 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 504 remove nil cons 528 def cons 529 def 44 ref 507 ref nil cons 530 def cons nil cons 531 def cons nil cons cons 532 def 61 ref subst 532 remove 127 ref subst nil 521 ref 531 ref cons nil cons cons 533 def 108 ref subst nil 529 remove 44 ref 45 ref 519 remove appTerm 507 remove appTerm 534 def nil cons 535 def cons nil cons 536 def cons nil cons cons 108 ref subst nil 177 ref 161 ref 45 ref 503 ref 164 ref appTerm 537 def appTerm 534 ref appTerm 538 def absTerm nil cons cons nil cons nil cons cons 525 ref subst 161 ref nil 74 ref 538 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 537 ref nil cons 539 def cons 536 ref cons nil cons cons 540 def 61 ref subst 540 remove 127 ref subst 537 ref betaConv 537 remove assume eqMp nil 43 ref 502 remove nil cons 541 def cons 542 def 536 remove cons nil cons cons 543 def 108 ref subst proveHyp 543 ref 61 ref subst 543 remove 127 ref subst 533 ref 61 ref subst 533 remove 127 ref subst nil 542 remove 531 remove cons nil cons cons 108 ref subst 514 ref 501 ref appTerm 544 def betaConv 516 ref 164 ref appTerm 545 def betaConv 518 ref 497 ref appTerm 546 def betaConv nil 521 remove 44 ref 546 remove nil cons cons nil cons cons nil cons cons 108 ref subst 176 ref 177 ref 518 remove nil cons cons 178 ref 497 ref nil cons cons nil cons 547 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 517 remove nil cons cons 44 ref 545 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 516 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 515 remove nil cons cons 44 ref 544 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 514 remove nil cons cons 178 ref 501 ref nil cons cons nil cons 548 def cons nil cons cons 138 ref subst eqMp eqMp eqMp eqMp nil 86 ref 520 remove cons 549 def 87 ref 530 remove cons nil cons 550 def cons nil cons cons 101 ref subst deductAntisym eqMp eqMp nil 86 ref 541 remove cons 87 ref 535 remove cons nil cons 551 def cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp nil 86 ref 539 remove cons 551 ref cons nil cons cons 101 ref subst deductAntisym eqMp eqMp absThm eqMp nil 43 ref 170 ref 178 ref 45 ref 503 ref 178 ref varTerm 552 def appTerm appTerm 534 ref appTerm absTerm appTerm nil cons cons 44 ref 505 remove 534 remove appTerm nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 503 remove nil cons cons 551 remove cons nil cons cons nil 485 remove 44 ref 45 ref 474 ref appTerm 553 def 92 ref appTerm nil cons 554 def cons nil cons cons nil cons cons 555 def 61 ref subst 555 remove 127 ref subst nil 43 ref 474 remove nil cons 556 def cons 557 def 487 remove cons nil cons cons 558 def 61 ref subst 558 remove 127 ref subst 488 remove 108 ref subst 44 ref 45 ref 117 ref 122 ref 479 remove 48 ref appTerm absTerm appTerm appTerm 48 ref appTerm absTerm 559 def 92 ref appTerm 560 def betaConv nil 557 remove 44 ref 200 ref 559 ref appTerm 561 def nil cons 562 def cons nil cons cons nil cons cons 563 def 108 ref subst 478 remove nil 43 ref 475 remove 561 ref appTerm nil cons cons 44 ref 553 remove 561 remove appTerm nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 563 remove nil 43 ref 335 remove nil cons 564 def cons 44 ref 338 ref cons nil cons cons nil cons cons 565 def 61 ref subst 565 remove 127 ref subst 337 remove eqMp nil 86 ref 564 remove cons 87 ref 338 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp subst eqMp eqMp nil 43 ref 562 remove cons 44 ref 560 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 559 remove nil cons cons 205 ref 486 remove cons nil cons cons nil cons cons 138 ref subst eqMp eqMp eqMp eqMp nil 86 ref 556 remove cons 491 remove cons nil cons cons 101 ref subst deductAntisym eqMp eqMp nil 490 remove 87 ref 554 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp 566 def subst eqMp eqMp eqMp eqMp nil 86 ref 528 remove cons 550 remove cons nil cons cons 101 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp nil 549 remove 87 ref 522 ref cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp nil 43 ref 522 remove cons 44 ref 513 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 524 remove 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 526 remove cons 44 ref 510 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 527 remove 548 ref cons nil cons cons 138 ref subst eqMp eqMp subst eqMp eqMp eqMp absThm eqMp nil 41 ref 450 remove appTerm thm nil 154 ref "w1" 2 ref var 567 def 6 ref "w2" 2 ref var 568 def 22 ref 144 ref 13 ref 567 ref varTerm 569 def appTerm 570 def appTerm 13 ref 568 ref varTerm 571 def appTerm 572 def appTerm 573 def appTerm 212 ref 569 ref appTerm 571 ref appTerm 574 def appTerm 575 def absTerm 576 def appTerm 577 def absTerm 578 def nil cons cons nil cons nil cons cons 197 ref 329 remove subst 579 def subst 567 ref nil 74 ref 577 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 576 remove nil cons cons nil cons nil cons cons 579 ref subst 568 ref nil 74 ref 575 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 573 ref nil cons 580 def cons 44 ref 574 ref nil cons 581 def cons nil cons 582 def cons nil cons cons 583 def 344 ref subst 583 ref 61 ref subst 583 ref 127 ref subst 273 ref nil 8 ref 569 ref nil cons 584 def cons nil cons nil cons cons 585 def 8 ref 212 ref 14 ref appTerm 303 remove appTerm 586 def absTerm 587 def 14 ref appTerm 588 def betaConv 7 ref 8 ref 586 remove assume sym 304 remove assume sym deductAntisym absThm appThm 302 remove eqMp nil 43 ref 6 ref 587 ref appTerm nil cons cons 44 ref 588 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 587 remove nil cons cons 156 ref cons nil cons cons 138 ref subst eqMp eqMp 589 def subst 590 def appThm nil 8 ref 571 ref nil cons 591 def cons nil cons 592 def nil cons cons 593 def 589 ref subst 594 def appThm sym 213 ref refl 595 def 573 ref assume appThm eqMp eqMp nil 86 ref 580 ref cons 87 ref 581 ref cons nil cons 596 def cons nil cons cons 101 ref subst deductAntisym eqMp 597 def nil 43 ref 45 ref 573 ref appTerm 574 ref appTerm 598 def nil cons 599 def cons 44 ref 45 ref 574 ref appTerm 573 remove appTerm nil cons cons nil cons cons nil cons cons 127 ref subst proveHyp nil 43 ref 581 ref cons 44 ref 580 ref cons nil cons 600 def cons nil cons cons 601 def 61 ref subst 601 remove 127 ref subst 22 ref "_31002" 2 ref var 602 def 144 ref 13 remove 602 remove varTerm appTerm appTerm 572 ref appTerm absTerm 603 def 569 ref appTerm 604 def appTerm refl 603 ref 571 ref appTerm betaConv appThm 89 ref 604 remove betaConv appThm 144 ref 572 ref appTerm 572 ref appTerm refl appThm trans 603 remove refl 574 ref assume appThm eqMp sym 572 ref refl eqMp eqMp nil 86 ref 581 remove cons 87 ref 580 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 6 ref 578 remove appTerm thm nil 154 ref 567 ref 6 ref 568 ref 598 remove absTerm 605 def appTerm 606 def absTerm 607 def nil cons cons nil cons nil cons cons 579 ref subst 567 ref nil 74 ref 606 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 605 remove nil cons cons nil cons nil cons cons 579 ref subst 568 ref nil 74 ref 599 remove cons nil cons nil cons cons 80 ref subst 597 ref eqMp absThm eqMp eqMp absThm eqMp nil 6 ref 607 remove appTerm thm nil 154 ref 567 ref 6 ref 568 ref 22 ref "Data.Word.Bits.compare" const 1 ref 3 ref 143 remove nil cons cons opType constTerm 608 def 370 ref appTerm 570 ref appTerm 572 ref appTerm appTerm 609 def "Data.Word.<" const 211 ref constTerm 610 def 569 ref appTerm 571 ref appTerm 611 def appTerm 612 def absTerm 613 def appTerm 614 def absTerm 615 def nil cons cons nil cons nil cons cons 579 ref subst 567 ref nil 74 ref 614 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 613 remove nil cons cons nil cons nil cons cons 579 ref subst 568 ref nil 74 ref 612 ref nil cons 616 def cons nil cons nil cons cons 617 def 80 ref subst 568 ref 609 ref 359 ref 1 ref 3 ref 21 ref nil cons cons opType constTerm 618 def 370 ref appTerm "Data.Word.<=" const 211 remove constTerm 619 def 569 ref appTerm 571 ref appTerm 620 def appTerm 611 ref appTerm appTerm 621 def absTerm 622 def 571 ref appTerm 623 def betaConv 567 ref 6 ref 622 ref appTerm 624 def absTerm 625 def 569 ref appTerm 626 def betaConv 44 ref 6 ref 567 ref 6 ref 568 ref 22 ref 608 ref 48 ref appTerm 627 def 570 ref appTerm 628 def 572 ref appTerm 629 def appTerm 630 def 618 ref 48 ref appTerm 631 def 620 ref appTerm 611 ref appTerm 632 def appTerm 633 def absTerm 634 def appTerm 635 def absTerm 636 def appTerm 637 def absTerm 638 def 370 ref appTerm 639 def betaConv nil 204 ref 638 ref nil cons cons 640 def nil cons nil cons cons 483 ref subst 44 ref nil 74 ref 637 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 636 remove nil cons cons nil cons nil cons cons 579 ref subst 567 ref nil 74 ref 635 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 634 remove nil cons cons nil cons nil cons cons 579 ref subst 568 ref nil 74 ref 633 ref nil cons 641 def cons nil cons nil cons cons 80 ref subst "l2" 10 ref var 642 def 45 ref 31 ref 35 ref 570 ref appTerm 643 def appTerm 644 def 35 ref 642 ref varTerm 645 def appTerm 646 def appTerm appTerm 22 ref 628 remove 645 ref appTerm appTerm "Number.Natural.Bits.compare" const 1 ref 3 ref 30 ref nil cons cons opType constTerm 647 def 48 ref appTerm 648 def 217 ref 570 ref appTerm 649 def appTerm 650 def 217 ref 645 ref appTerm 651 def appTerm appTerm appTerm absTerm 652 def 572 ref appTerm 653 def betaConv "l1" 10 ref var 654 def 41 ref 642 ref 45 ref 31 ref 35 ref 654 ref varTerm 655 def appTerm 656 def appTerm 646 ref appTerm appTerm 22 ref 627 ref 655 ref appTerm 645 ref appTerm appTerm 648 ref 217 ref 655 ref appTerm 657 def appTerm 651 ref appTerm appTerm appTerm absTerm appTerm 658 def absTerm 659 def 570 ref appTerm 660 def betaConv 44 ref 41 ref 659 ref appTerm 661 def absTerm 662 def 48 ref appTerm 663 def betaConv 89 ref 200 ref refl 664 def 44 ref 41 ref refl 665 def 654 ref 44 ref 659 ref absTerm 666 def 48 ref appTerm betaConv 655 ref refl appThm 659 ref 655 ref appTerm betaConv trans 667 def absThm appThm absThm appThm appThm 665 ref 654 ref 664 ref 44 ref 667 remove absThm appThm absThm appThm appThm nil "p" 1 ref 3 ref 142 remove cons opType var 666 remove nil cons cons nil cons nil cons cons "B" 12 remove cons 203 ref cons 186 ref cons "p" 1 ref 114 ref 1 ref "B" varType 668 def 4 ref cons opType 669 def nil cons 670 def cons opType 671 def var 672 def 22 ref 117 ref 122 ref 0 ref 1 ref 669 remove 4 ref cons opType constTerm 673 def "y" 668 ref var 674 def 672 remove varTerm 675 def 123 ref appTerm 674 ref varTerm appTerm 676 def absTerm appTerm absTerm appTerm appTerm 673 remove 674 remove 117 ref 122 ref 676 remove absTerm appTerm absTerm appTerm appTerm absTerm 677 def 675 ref appTerm 678 def betaConv nil 0 ref 1 ref 1 ref 671 ref 4 ref cons opType 679 def 4 ref cons opType constTerm 677 ref appTerm 680 def axiom nil 43 ref 680 remove nil cons cons 44 ref 678 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp "A" 671 ref nil cons cons nil cons "P" 679 remove var 677 remove nil cons cons "x" 671 remove var 675 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp subst subst eqMp sym nil 204 ref 44 ref 41 ref 642 ref 45 ref 31 ref 35 ref 210 ref appTerm 681 def appTerm 646 ref appTerm appTerm 22 ref 627 ref 210 ref appTerm 682 def 645 ref appTerm appTerm 648 ref 225 ref appTerm 683 def 651 ref appTerm appTerm 684 def appTerm 685 def absTerm 686 def appTerm 687 def absTerm 688 def nil cons cons nil cons nil cons cons 483 ref subst 44 ref nil 74 ref 687 remove nil cons cons nil cons nil cons cons 80 ref subst nil 110 ref 686 remove nil cons cons nil cons nil cons cons 330 ref subst 642 ref nil 74 ref 685 remove nil cons cons nil cons nil cons cons 80 ref subst 45 ref refl 689 def nil "y" 27 ref var 690 def 646 ref nil cons cons 178 ref 681 ref nil cons cons nil cons cons nil cons cons 187 ref "y" 114 ref var 691 def 22 ref 190 remove 691 ref varTerm 692 def appTerm appTerm 189 ref 692 ref appTerm 123 ref appTerm appTerm absTerm 693 def 692 ref appTerm 694 def betaConv 122 ref 117 ref 693 ref appTerm 695 def absTerm 696 def 123 ref appTerm 697 def betaConv nil 117 ref 696 ref appTerm 698 def axiom nil 43 ref 698 remove nil cons cons 44 ref 697 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 696 remove nil cons cons 415 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 695 remove nil cons cons 44 ref 694 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 693 remove nil cons cons 122 ref 692 ref nil cons cons nil cons 699 def cons nil cons cons 138 ref subst eqMp eqMp subst subst appThm 684 ref refl 700 def appThm sym 689 ref 31 ref 646 ref appTerm refl 402 ref nil 31 ref 32 ref 1 ref 404 ref 33 ref cons opType constTerm 701 def 410 ref appTerm appTerm 226 ref appTerm axiom subst 702 def appThm nil 11 ref 645 ref nil cons 703 def cons nil cons nil cons cons 402 ref 416 ref 22 ref 31 ref 701 ref 418 ref appTerm 704 def appTerm 226 ref appTerm appTerm 407 ref 418 ref appTerm 410 ref appTerm appTerm absTerm 705 def 418 ref appTerm 706 def betaConv nil 422 ref 705 ref appTerm 707 def axiom nil 43 ref 707 remove nil cons cons 44 ref 706 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 424 ref 425 ref 705 remove nil cons cons 427 ref cons nil cons cons 138 ref subst eqMp eqMp subst subst trans appThm 700 remove appThm sym nil 43 ref 144 ref 645 ref appTerm 210 ref appTerm 708 def nil cons 709 def cons 44 ref 684 remove nil cons 710 def cons nil cons cons nil cons cons 711 def 61 ref subst 711 remove 127 ref subst 22 ref "_31012" 10 ref var 712 def 22 ref 682 ref 712 remove varTerm 713 def appTerm appTerm 683 ref 217 ref 713 remove appTerm appTerm appTerm absTerm 714 def 645 ref appTerm 715 def appTerm refl 714 ref 210 ref appTerm betaConv appThm 89 ref 715 remove betaConv appThm 22 ref 682 remove 210 ref appTerm appTerm 716 def 683 remove 225 ref appTerm appTerm refl appThm trans 714 remove refl 708 remove assume appThm eqMp sym 89 ref 44 ref 716 remove 48 ref appTerm absTerm 717 def 48 ref appTerm 718 def betaConv nil 200 ref 717 ref appTerm 719 def axiom nil 43 ref 719 remove nil cons cons 44 ref 718 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 717 remove nil cons cons 205 ref 82 remove cons nil cons 720 def cons nil cons cons 138 ref subst eqMp eqMp appThm 648 ref refl 721 def 227 ref appThm 227 remove appThm 233 remove 161 ref 22 ref 648 ref 226 ref appTerm 164 ref appTerm appTerm "Data.Bool.\\/" const 21 ref constTerm 722 def 48 ref appTerm 723 def "Data.Bool.~" const 20 ref constTerm 724 def 31 ref 164 ref appTerm 226 ref appTerm appTerm appTerm appTerm absTerm 725 def 164 ref appTerm 726 def betaConv 44 ref 170 ref 725 ref appTerm 727 def absTerm 728 def 48 ref appTerm 729 def betaConv nil 200 ref 728 ref appTerm 730 def axiom nil 43 ref 730 remove nil cons cons 44 ref 729 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 728 remove nil cons cons 720 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 727 remove nil cons cons 44 ref 726 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 725 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst 723 ref refl 724 ref refl 731 def nil 178 ref 232 ref cons 732 def nil cons nil cons cons 192 ref subst appThm nil 22 ref 724 ref 66 ref appTerm appTerm 370 ref appTerm axiom trans appThm 83 remove 74 ref 22 ref 722 ref 76 ref appTerm 733 def 370 ref appTerm appTerm 76 ref appTerm absTerm 734 def 76 ref appTerm 735 def betaConv nil 200 ref 734 ref appTerm 736 def axiom nil 43 ref 736 remove nil cons cons 44 ref 735 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 734 remove nil cons cons 206 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans trans trans appThm nil 720 ref nil cons cons 402 ref 191 ref subst 737 def subst trans sym 79 ref eqMp eqMp eqMp nil 86 ref 709 remove cons 87 ref 710 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 43 ref 200 ref 688 remove appTerm 738 def nil cons cons 44 ref 200 ref "h" 3 ref var 739 def 41 ref "t" 10 ref var 740 def 45 ref 200 ref 44 ref 41 ref 642 ref 45 ref 31 ref 35 ref 740 ref varTerm 741 def appTerm 742 def appTerm 743 def 646 ref appTerm appTerm 22 ref 627 ref 741 ref appTerm 645 ref appTerm appTerm 648 ref 217 ref 741 ref appTerm 744 def appTerm 651 ref appTerm appTerm appTerm absTerm 745 def appTerm 746 def absTerm 747 def appTerm 748 def appTerm 200 ref 44 ref 41 ref 642 ref 45 ref 31 ref 35 ref "Data.List.::" const 749 def 1 ref 3 ref 360 ref cons opType constTerm 750 def 739 ref varTerm 751 def appTerm 741 ref appTerm 752 def appTerm appTerm 753 def 646 remove appTerm appTerm 22 ref 627 ref 752 ref appTerm 754 def 645 ref appTerm appTerm 648 ref 217 ref 752 ref appTerm 755 def appTerm 756 def 651 ref appTerm appTerm appTerm absTerm 757 def appTerm 758 def absTerm 759 def appTerm 760 def appTerm 761 def absTerm 762 def appTerm 763 def absTerm 764 def appTerm 765 def nil cons cons nil cons cons nil cons cons 127 ref subst proveHyp nil 204 ref 764 remove nil cons cons nil cons nil cons cons 483 ref subst 739 ref nil 74 ref 763 remove nil cons cons nil cons nil cons cons 80 ref subst nil 110 ref 762 remove nil cons cons nil cons nil cons cons 330 ref subst 740 ref nil 74 ref 761 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 748 remove nil cons 766 def cons 767 def 44 ref 760 remove nil cons 768 def cons nil cons cons nil cons cons 769 def 61 ref subst 769 remove 127 ref subst nil 204 ref 759 remove nil cons cons nil cons nil cons cons 483 ref subst 44 ref nil 74 ref 758 remove nil cons 770 def cons nil cons nil cons cons 80 ref subst 689 ref 140 ref 402 ref "t" 404 ref var 771 def 31 ref 701 ref 749 remove 1 ref 114 ref 417 ref cons opType constTerm "h" 114 ref var 772 def varTerm 773 def appTerm 771 ref varTerm 774 def appTerm 775 def appTerm appTerm "Number.Natural.suc" const 235 remove constTerm 776 def 701 ref 774 ref appTerm appTerm appTerm absTerm 777 def 774 ref appTerm 778 def betaConv 772 ref 422 ref 777 ref appTerm 779 def absTerm 780 def 773 ref appTerm 781 def betaConv nil 117 ref 780 ref appTerm 782 def axiom nil 43 ref 782 remove nil cons cons 44 ref 781 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 780 remove nil cons cons 122 ref 773 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 779 remove nil cons cons 44 ref 778 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 424 ref 425 ref 777 remove nil cons cons 426 ref 774 ref nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp subst 783 def appThm 784 def 702 remove appThm nil 161 ref 742 remove nil cons 785 def cons nil cons nil cons cons 161 ref 724 ref 31 ref 776 ref 164 ref appTerm 786 def appTerm 226 ref appTerm 787 def appTerm 788 def absTerm 789 def 164 ref appTerm 790 def betaConv nil 170 ref 789 ref appTerm 791 def axiom nil 43 ref 791 remove nil cons cons 44 ref 790 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 789 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 788 remove nil cons cons 44 ref 22 ref 787 ref appTerm 370 ref appTerm nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp nil 86 ref 787 remove nil cons cons nil cons nil cons cons nil 43 ref 724 ref 90 ref appTerm 792 def nil cons 793 def cons 44 ref 22 ref 90 ref appTerm 370 ref appTerm nil cons 794 def cons nil cons cons nil cons cons 795 def 61 ref subst 795 remove 127 ref subst nil 43 ref 90 ref nil cons 796 def cons 44 ref 399 ref cons nil cons 797 def cons nil cons cons 344 remove subst 22 ref 792 ref appTerm refl 43 ref 47 ref 370 ref appTerm absTerm 798 def 90 ref appTerm betaConv appThm nil 70 ref 724 ref appTerm 798 remove appTerm axiom 99 ref appThm eqMp 792 remove assume eqMp nil 43 ref 45 ref 90 ref appTerm 799 def 370 ref appTerm nil cons cons 44 ref 45 ref 370 ref appTerm 800 def 90 ref appTerm nil cons cons nil cons cons nil cons cons 127 ref subst proveHyp nil 43 ref 399 ref cons 44 ref 796 ref cons nil cons cons nil cons cons 801 def 61 ref subst 801 remove 127 ref subst 43 ref 46 ref absTerm 802 def 90 ref appTerm 803 def betaConv nil 22 ref 370 ref appTerm 804 def 200 ref 802 ref appTerm 805 def appTerm axiom 370 ref assume eqMp nil 43 ref 805 remove nil cons cons 44 ref 803 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 802 remove nil cons cons 205 ref 796 ref cons nil cons cons nil cons cons 138 ref subst eqMp eqMp 806 def eqMp nil 86 ref 399 ref cons 87 ref 796 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 86 ref 793 remove cons 87 ref 794 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp 807 def subst eqMp subst trans appThm 22 ref 754 ref 210 ref appTerm appTerm 756 ref 225 remove appTerm appTerm 808 def refl appThm nil 74 ref 808 ref nil cons cons nil cons nil cons cons 74 ref 22 ref 800 remove 76 ref appTerm appTerm 66 ref appTerm absTerm 809 def 76 ref appTerm 810 def betaConv nil 200 ref 809 ref appTerm 811 def axiom nil 43 ref 811 remove nil cons cons 44 ref 810 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 809 remove nil cons cons 206 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans sym 79 ref eqMp nil 43 ref 45 ref 753 ref 681 remove appTerm appTerm 808 remove appTerm 812 def nil cons cons 44 ref 200 ref "h'" 3 ref var 813 def 41 ref "t'" 10 ref var 814 def 45 ref 45 ref 753 ref 35 ref 814 ref varTerm 815 def appTerm 816 def appTerm appTerm 22 ref 754 ref 815 ref appTerm appTerm 756 ref 217 ref 815 ref appTerm 817 def appTerm appTerm appTerm 818 def appTerm 45 ref 753 remove 35 ref 750 ref 813 ref varTerm 819 def appTerm 815 ref appTerm 820 def appTerm appTerm appTerm 22 ref 754 remove 820 ref appTerm appTerm 756 remove 217 ref 820 ref appTerm appTerm appTerm 821 def appTerm 822 def appTerm 823 def absTerm 824 def appTerm 825 def absTerm 826 def appTerm 827 def nil cons cons nil cons cons nil cons cons 127 ref subst proveHyp nil 204 ref 826 remove nil cons cons nil cons nil cons cons 483 ref subst 813 ref nil 74 ref 825 remove nil cons cons nil cons nil cons cons 80 ref subst nil 110 ref 824 remove nil cons cons nil cons nil cons cons 330 ref subst 814 ref nil 74 ref 823 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 818 remove nil cons 828 def cons 44 ref 822 remove nil cons 829 def cons nil cons cons nil cons cons 830 def 61 ref subst 830 remove 127 ref subst 689 ref 784 remove nil 740 ref 815 ref nil cons 831 def cons 739 ref 819 ref nil cons 832 def cons nil cons cons nil cons cons 833 def 783 remove subst appThm nil 161 ref 816 ref nil cons cons 495 ref 785 remove cons nil cons cons nil cons cons 161 ref 22 ref 31 ref 776 remove 497 ref appTerm appTerm 786 remove appTerm appTerm 31 ref 497 ref appTerm 164 ref appTerm 834 def appTerm absTerm 835 def 164 ref appTerm 836 def betaConv 495 ref 170 ref 835 ref appTerm 837 def absTerm 838 def 497 ref appTerm 839 def betaConv nil 170 ref 838 ref appTerm 840 def axiom nil 43 ref 840 remove nil cons cons 44 ref 839 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 838 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 837 remove nil cons cons 44 ref 836 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 835 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans appThm 821 ref refl appThm sym nil 43 ref 743 remove 816 remove appTerm nil cons 841 def cons 842 def 44 ref 821 remove nil cons 843 def cons nil cons cons nil cons cons 844 def 61 ref subst 844 remove 127 ref subst 89 ref nil 429 ref 831 ref cons "h2" 3 ref var 845 def 832 remove cons 846 def 431 ref 741 ref nil cons 847 def cons "h1" 3 ref var 848 def 751 ref nil cons 849 def cons nil cons 850 def cons cons cons nil cons cons 429 ref 22 ref 627 remove 750 ref 848 ref varTerm 851 def appTerm 431 ref varTerm 852 def appTerm appTerm 750 remove 845 ref varTerm 853 def appTerm 429 remove varTerm 854 def appTerm appTerm appTerm 608 ref 722 ref 50 ref 724 ref 851 ref appTerm appTerm 853 ref appTerm appTerm 50 ref 724 ref 50 ref 851 ref appTerm 724 ref 853 ref appTerm appTerm appTerm appTerm 48 ref appTerm appTerm 855 def appTerm 852 ref appTerm 854 ref appTerm appTerm absTerm 856 def 854 ref appTerm 857 def betaConv 431 remove 41 ref 856 ref appTerm 858 def absTerm 859 def 852 ref appTerm 860 def betaConv 845 ref 41 ref 859 ref appTerm 861 def absTerm 862 def 853 ref appTerm 863 def betaConv 848 ref 200 ref 862 ref appTerm 864 def absTerm 865 def 851 ref appTerm 866 def betaConv 44 ref 200 ref 865 ref appTerm 867 def absTerm 868 def 48 ref appTerm 869 def betaConv nil 200 ref 868 ref appTerm 870 def axiom nil 43 ref 870 remove nil cons cons 44 ref 869 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 868 remove nil cons cons 720 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 867 remove nil cons cons 44 ref 866 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 865 remove nil cons cons 205 ref 851 ref nil cons cons nil cons 871 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 864 remove nil cons cons 44 ref 863 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 862 remove nil cons cons 205 ref 853 ref nil cons cons nil cons 872 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 861 remove nil cons cons 44 ref 860 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 859 remove nil cons cons 111 ref 852 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 858 remove nil cons cons 44 ref 857 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 856 remove nil cons cons 111 ref 854 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp subst appThm 721 remove 740 ref 31 ref 755 remove appTerm "Number.Natural.Bits.cons" const 1 ref 3 ref 236 remove cons opType constTerm 873 def 751 ref appTerm 874 def 744 ref appTerm appTerm absTerm 875 def 741 ref appTerm 876 def betaConv 739 ref 41 ref 875 ref appTerm 877 def absTerm 878 def 751 ref appTerm 879 def betaConv nil 200 ref 878 ref appTerm 880 def axiom nil 43 ref 880 remove nil cons cons 44 ref 879 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 878 remove nil cons cons 205 ref 849 ref cons nil cons 881 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 877 remove nil cons cons 44 ref 876 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 875 remove nil cons cons 111 ref 847 ref cons nil cons cons nil cons cons 138 ref subst eqMp eqMp 882 def appThm 833 remove 882 ref subst appThm nil "t2" 27 ref var 883 def 817 ref nil cons cons 846 remove "t1" 27 ref var 884 def 744 ref nil cons 885 def cons 850 remove cons cons cons nil cons cons 883 ref 22 ref 648 ref 873 ref 851 ref appTerm 884 ref varTerm 886 def appTerm appTerm 873 remove 853 ref appTerm 883 ref varTerm 887 def appTerm appTerm appTerm 647 ref 855 remove appTerm 886 ref appTerm 887 ref appTerm appTerm absTerm 888 def 887 ref appTerm 889 def betaConv 884 ref 170 ref 888 ref appTerm 890 def absTerm 891 def 886 ref appTerm 892 def betaConv 845 remove 170 ref 891 ref appTerm 893 def absTerm 894 def 853 remove appTerm 895 def betaConv 848 remove 200 ref 894 ref appTerm 896 def absTerm 897 def 851 remove appTerm 898 def betaConv 44 ref 200 ref 897 ref appTerm 899 def absTerm 900 def 48 ref appTerm 901 def betaConv nil 200 ref 900 ref appTerm 902 def axiom nil 43 ref 902 remove nil cons cons 44 ref 901 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 900 remove nil cons cons 720 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 899 remove nil cons cons 44 ref 898 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 897 remove nil cons cons 871 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 896 remove nil cons cons 44 ref 895 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 894 remove nil cons cons 872 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 893 remove nil cons cons 44 ref 892 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 891 remove nil cons cons 178 ref 886 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 890 remove nil cons cons 44 ref 889 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 888 remove nil cons cons 178 ref 887 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp subst trans appThm sym nil 842 remove 44 ref 22 ref 608 ref 722 ref 50 ref 724 ref 751 ref appTerm appTerm 819 ref appTerm appTerm 50 ref 724 ref 50 ref 751 ref appTerm 724 ref 819 remove appTerm appTerm appTerm appTerm 48 ref appTerm appTerm 903 def appTerm 741 ref appTerm 815 ref appTerm appTerm 647 remove 903 ref appTerm 744 ref appTerm 817 remove appTerm appTerm nil cons cons nil cons cons nil cons cons 108 ref subst nil 642 ref 831 remove cons 44 ref 903 remove nil cons cons nil cons cons nil cons cons 745 ref 645 ref appTerm 904 def betaConv 747 ref 48 ref appTerm 905 def betaConv nil 767 remove 44 ref 905 remove nil cons cons nil cons cons nil cons cons 108 ref subst 203 ref 204 ref 747 remove nil cons cons 720 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 746 remove nil cons cons 44 ref 904 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 745 remove nil cons cons 111 ref 703 remove cons nil cons 906 def cons nil cons cons 138 ref subst eqMp eqMp subst eqMp eqMp eqMp nil 86 ref 841 remove cons 87 ref 843 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp nil 86 ref 828 remove cons 87 ref 829 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp nil 43 ref 50 ref 812 remove appTerm 827 remove appTerm nil cons cons 44 ref 770 remove cons nil cons cons nil cons cons 108 ref subst proveHyp 689 ref 455 ref 757 ref 210 ref appTerm betaConv appThm 664 ref 813 remove 665 ref 814 remove 689 ref 757 ref 815 remove appTerm betaConv appThm 757 ref 820 remove appTerm betaConv appThm absThm appThm absThm appThm appThm appThm 665 ref 642 ref 757 ref 645 ref appTerm betaConv absThm appThm appThm nil "p" 23 ref var 907 def 757 remove nil cons cons nil cons nil cons cons 402 ref "p" 405 ref var 908 def 45 ref 50 ref 908 remove varTerm 909 def 410 remove appTerm appTerm 117 ref 772 remove 422 ref 771 remove 45 ref 909 ref 774 remove appTerm appTerm 909 ref 775 remove appTerm appTerm absTerm appTerm absTerm appTerm appTerm appTerm 422 ref 416 ref 909 ref 418 ref appTerm absTerm appTerm appTerm absTerm 910 def 909 ref appTerm 911 def betaConv nil 0 ref 1 ref 421 ref 4 ref cons opType constTerm 910 ref appTerm 912 def axiom nil 43 ref 912 remove nil cons cons 44 ref 911 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp "A" 406 remove cons nil cons "P" 421 remove var 910 remove nil cons cons "x" 405 remove var 909 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp subst 913 def subst eqMp eqMp eqMp absThm eqMp eqMp nil 86 ref 766 remove cons 87 ref 768 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp nil 43 ref 50 ref 738 remove appTerm 765 remove appTerm nil cons cons 44 ref 41 ref 654 ref 200 ref 44 ref 658 remove absTerm appTerm absTerm 914 def appTerm nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 689 ref 455 ref 914 ref 210 remove appTerm betaConv appThm 664 ref 739 ref 665 ref 740 ref 689 ref 914 ref 741 ref appTerm betaConv appThm 914 ref 752 ref appTerm betaConv appThm absThm appThm absThm appThm appThm appThm 665 ref 654 ref 914 ref 655 ref appTerm betaConv absThm appThm appThm nil 907 remove 914 remove nil cons cons nil cons nil cons cons 913 remove subst eqMp eqMp eqMp 915 def nil 43 ref 200 ref 662 ref appTerm 916 def nil cons cons 44 ref 663 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 662 remove nil cons cons 720 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 661 remove nil cons cons 44 ref 660 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 659 remove nil cons cons 111 ref 570 ref nil cons 917 def cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 41 ref 652 ref appTerm nil cons cons 44 ref 653 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 652 remove nil cons cons 111 ref 572 ref nil cons 918 def cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 45 ref 644 remove 35 ref 572 ref appTerm 919 def appTerm 920 def appTerm 630 remove 650 remove 217 ref 572 ref appTerm 921 def appTerm 922 def appTerm 923 def appTerm nil cons cons 44 ref 641 ref cons nil cons 924 def cons nil cons cons 108 ref subst proveHyp 689 ref 689 ref 140 ref 585 ref 183 ref subst 925 def appThm 593 ref 183 ref subst 926 def appThm 193 remove trans 927 def appThm 923 ref refl appThm nil 74 ref 923 ref nil cons 928 def cons nil cons nil cons cons 74 ref 22 ref 45 ref 66 ref appTerm 76 ref appTerm appTerm 76 ref appTerm absTerm 929 def 76 ref appTerm 930 def betaConv nil 200 ref 929 ref appTerm 931 def axiom nil 43 ref 931 remove nil cons cons 44 ref 930 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 929 remove nil cons cons 206 ref cons nil cons cons 138 ref subst eqMp eqMp 932 def subst trans appThm 633 remove refl appThm sym nil 43 ref 928 ref cons 924 remove cons nil cons cons 933 def 61 ref subst 933 remove 127 ref subst 22 ref "_31014" 3 ref var 934 def 22 ref 934 remove varTerm appTerm 632 ref appTerm absTerm 935 def 629 remove appTerm 936 def appTerm refl 935 ref 922 ref appTerm betaConv appThm 89 ref 936 remove betaConv appThm 22 ref 922 remove appTerm 632 remove appTerm refl appThm trans 935 remove refl 923 remove assume appThm eqMp sym 89 ref nil 161 ref 921 remove nil cons cons 495 ref 649 remove nil cons cons nil cons cons nil cons cons 161 ref 22 ref 648 remove 497 ref appTerm 164 ref appTerm appTerm 631 ref 499 ref appTerm 506 remove 164 ref appTerm 937 def appTerm appTerm absTerm 938 def 164 ref appTerm 939 def betaConv 495 ref 170 ref 938 ref appTerm 940 def absTerm 941 def 497 ref appTerm 942 def betaConv 44 ref 170 ref 941 ref appTerm 943 def absTerm 944 def 48 ref appTerm 945 def betaConv nil 200 ref 944 ref appTerm 946 def axiom nil 43 ref 946 remove nil cons cons 44 ref 945 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 944 remove nil cons cons 720 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 943 remove nil cons cons 44 ref 942 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 941 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 940 remove nil cons cons 44 ref 939 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 938 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst 631 ref refl 947 def 383 ref 585 ref 293 ref subst 948 def appThm 593 ref 293 remove subst 949 def appThm appThm 451 remove 948 remove appThm 949 remove appThm appThm trans appThm 947 remove nil "y" 2 ref var 950 def 591 ref cons 155 ref 584 remove cons nil cons 951 def cons nil cons cons 952 def 950 ref 22 ref 619 remove 286 ref appTerm 950 ref varTerm 953 def appTerm appTerm 306 ref 287 ref appTerm 147 ref 953 ref appTerm 954 def appTerm appTerm absTerm 955 def 953 ref appTerm 956 def betaConv 155 ref 6 ref 955 ref appTerm 957 def absTerm 958 def 286 ref appTerm 959 def betaConv nil 6 ref 958 ref appTerm 960 def axiom nil 43 ref 960 remove nil cons cons 44 ref 959 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 958 remove nil cons cons 291 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 957 remove nil cons cons 44 ref 956 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 955 remove nil cons cons 155 ref 953 ref nil cons cons nil cons 961 def cons nil cons cons 138 ref subst eqMp eqMp subst appThm 952 remove 950 ref 22 ref 610 remove 286 ref appTerm 953 ref appTerm appTerm 317 remove 954 ref appTerm appTerm absTerm 962 def 953 ref appTerm 963 def betaConv 155 ref 6 ref 962 ref appTerm 964 def absTerm 965 def 286 ref appTerm 966 def betaConv nil 6 ref 965 ref appTerm 967 def axiom nil 43 ref 967 remove nil cons cons 44 ref 966 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 965 remove nil cons cons 291 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 964 remove nil cons cons 44 ref 963 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 962 remove nil cons cons 961 ref cons nil cons cons 138 ref subst eqMp eqMp subst appThm appThm nil 205 ref 631 remove 306 ref 147 ref 569 ref appTerm 968 def appTerm 147 ref 571 ref appTerm 969 def appTerm appTerm 309 ref 968 ref appTerm 969 ref appTerm appTerm nil cons cons nil cons nil cons cons 737 ref subst trans sym 79 ref eqMp eqMp eqMp nil 86 ref 928 remove cons 87 ref 641 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp 970 def nil 43 ref 200 ref 638 ref appTerm 971 def nil cons cons 972 def 44 ref 639 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 640 ref 400 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 6 ref 625 ref appTerm nil cons cons 44 ref 626 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 625 remove nil cons cons 951 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 624 remove nil cons cons 44 ref 623 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 622 remove nil cons cons 155 ref 591 remove cons nil cons 973 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 621 remove nil cons cons 44 ref 616 remove cons nil cons cons nil cons cons 108 ref subst proveHyp 689 ref 609 remove refl nil "t2" 3 ref var 974 def 611 ref nil cons cons "t1" 3 ref var 975 def 620 ref nil cons cons nil cons cons nil cons cons 976 def 402 ref 432 remove 189 ref 433 ref 370 ref appTerm 435 ref appTerm 436 ref appTerm appTerm 436 ref appTerm absTerm 977 def 436 remove appTerm 978 def betaConv 434 remove 117 ref 977 ref appTerm 979 def absTerm 980 def 435 remove appTerm 981 def betaConv nil 117 ref 980 ref appTerm 982 def axiom nil 43 ref 982 remove nil cons cons 44 ref 981 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 980 remove nil cons cons 443 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 979 remove nil cons cons 44 ref 978 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 977 remove nil cons cons 444 remove cons nil cons cons 138 ref subst eqMp eqMp 983 def subst subst appThm appThm 612 remove refl appThm 617 remove nil 74 ref 45 ref 76 ref appTerm 984 def 76 ref appTerm 985 def nil cons cons nil cons nil cons cons 80 ref subst 74 ref 985 remove absTerm 986 def 76 ref appTerm 987 def betaConv nil 200 ref 986 ref appTerm 988 def axiom nil 43 ref 988 remove nil cons cons 44 ref 987 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 986 remove nil cons cons 206 ref cons nil cons cons 138 ref subst eqMp eqMp eqMp 989 def subst trans sym 79 ref eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 6 ref 615 remove appTerm thm nil 154 ref 567 ref 6 ref 568 ref 22 ref 608 remove 66 ref appTerm 570 ref appTerm 572 ref appTerm appTerm 990 def 620 ref appTerm 991 def absTerm 992 def appTerm 993 def absTerm 994 def nil cons cons nil cons nil cons cons 579 ref subst 567 ref nil 74 ref 993 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 992 remove nil cons cons nil cons nil cons cons 579 ref subst 568 ref nil 74 ref 991 ref nil cons 995 def cons nil cons nil cons cons 996 def 80 ref subst 568 ref 990 ref 618 remove 66 ref appTerm 620 remove appTerm 611 remove appTerm appTerm 997 def absTerm 998 def 571 ref appTerm 999 def betaConv 567 ref 6 ref 998 ref appTerm 1000 def absTerm 1001 def 569 ref appTerm 1002 def betaConv 638 remove 66 ref appTerm 1003 def betaConv 970 ref nil 972 remove 44 ref 1003 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 640 remove 205 ref 195 remove cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 6 ref 1001 ref appTerm nil cons cons 44 ref 1002 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1001 remove nil cons cons 951 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1000 remove nil cons cons 44 ref 999 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 998 remove nil cons cons 973 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 997 remove nil cons cons 44 ref 995 remove cons nil cons cons nil cons cons 108 ref subst proveHyp 689 ref 990 remove refl 976 remove 402 ref 445 ref subst subst appThm appThm 991 remove refl appThm 996 remove 989 ref subst trans sym 79 ref eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 6 ref 994 remove appTerm thm nil 154 ref 567 ref 6 ref 568 ref 212 ref "Data.Word.and" const 1 ref 2 ref 1 ref 2 ref 152 ref cons opType 1004 def nil cons cons opType 1005 def constTerm 569 ref appTerm 571 ref appTerm 1006 def appTerm 1007 def 213 ref "Data.List.zipWith" const 1 ref 21 remove 362 remove cons opType constTerm 1008 def 50 ref appTerm 1009 def 570 ref appTerm 572 ref appTerm 1010 def appTerm 1011 def appTerm 1012 def absTerm 1013 def appTerm 1014 def absTerm 1015 def nil cons cons nil cons nil cons cons 579 ref subst 567 ref nil 74 ref 1014 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 1013 remove nil cons cons nil cons nil cons cons 579 ref subst 568 ref nil 74 ref 1012 remove nil cons cons nil cons nil cons cons 80 ref subst 273 ref nil 155 ref 1006 ref nil cons 1016 def cons nil cons nil cons cons 155 ref 212 ref 286 ref appTerm 1017 def 294 remove appTerm 1018 def absTerm 1019 def 286 ref appTerm 1020 def betaConv 7 remove 155 ref 1018 remove assume sym 295 remove assume sym deductAntisym absThm appThm 299 remove eqMp nil 43 ref 6 ref 1019 ref appTerm nil cons cons 44 ref 1020 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1019 remove nil cons cons 291 ref cons nil cons cons 138 ref subst eqMp eqMp 1021 def subst appThm 1011 remove refl appThm sym 273 ref 224 ref 231 ref 568 ref 1007 remove 216 ref "Number.Natural.Bits.and" const 237 ref constTerm 1022 def 968 ref appTerm 969 ref appTerm 1023 def appTerm appTerm absTerm 1024 def 571 ref appTerm 1025 def betaConv 567 ref 6 ref 1024 ref appTerm 1026 def absTerm 1027 def 569 ref appTerm 1028 def betaConv nil 6 ref 1027 ref appTerm 1029 def axiom nil 43 ref 1029 remove nil cons cons 44 ref 1028 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1027 remove nil cons cons 951 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1026 remove nil cons cons 44 ref 1025 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1024 remove nil cons cons 973 ref cons nil cons cons 138 ref subst eqMp eqMp appThm nil 161 ref 1023 ref nil cons cons nil cons 1030 def nil cons cons 269 ref subst trans 1031 def appThm appThm nil 11 ref 1010 remove nil cons cons nil cons nil cons cons 223 ref subst 224 ref 274 ref 1009 ref refl 585 remove 157 ref subst 1032 def appThm 593 remove 157 remove subst 1033 def appThm nil 161 ref 969 ref nil cons cons 1034 def 160 ref 495 ref 968 ref nil cons 1035 def cons nil cons 1036 def cons cons nil cons cons 1037 def 158 ref 144 ref 1009 remove 146 ref 497 ref appTerm 165 ref appTerm 1038 def appTerm 166 ref appTerm 1039 def appTerm 146 ref 1022 remove 497 ref appTerm 164 ref appTerm 1040 def appTerm 165 ref appTerm 1041 def appTerm 1042 def absTerm 1043 def 165 ref appTerm 1044 def betaConv 161 ref 170 ref 1043 ref appTerm 1045 def absTerm 1046 def 164 ref appTerm 1047 def betaConv 495 ref 170 ref 1046 ref appTerm 1048 def absTerm 1049 def 497 ref appTerm 1050 def betaConv 242 ref 495 ref 242 ref 161 ref 242 ref 158 ref 1042 remove assume sym 144 ref 1041 remove appTerm 1039 remove appTerm 1051 def assume sym deductAntisym absThm appThm absThm appThm absThm appThm nil 170 ref 495 ref 170 ref 161 ref 170 ref 158 ref 1051 remove absTerm appTerm absTerm appTerm absTerm appTerm axiom eqMp nil 43 ref 170 ref 1049 ref appTerm nil cons cons 44 ref 1050 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1049 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1048 remove nil cons cons 44 ref 1047 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1046 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1045 remove nil cons cons 44 ref 1044 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1043 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans appThm nil 160 ref 1030 remove cons 1052 def nil cons cons 282 ref subst trans appThm trans appThm nil 155 ref 216 ref 238 ref 1023 remove appTerm 37 ref appTerm appTerm nil cons cons nil cons nil cons cons 301 ref subst trans sym 79 ref eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 6 ref 1015 remove appTerm thm nil 154 ref 567 ref 6 ref 568 ref 212 ref "Data.Word.or" const 1005 ref constTerm 569 ref appTerm 571 ref appTerm 1053 def appTerm 1054 def 213 ref 1008 remove 722 ref appTerm 1055 def 570 ref appTerm 572 ref appTerm 1056 def appTerm 1057 def appTerm 1058 def absTerm 1059 def appTerm 1060 def absTerm 1061 def nil cons cons nil cons nil cons cons 579 ref subst 567 ref nil 74 ref 1060 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 1059 remove nil cons cons nil cons nil cons cons 579 ref subst 568 ref nil 74 ref 1058 remove nil cons cons nil cons nil cons cons 80 ref subst 273 ref nil 155 ref 1053 ref nil cons 1062 def cons nil cons nil cons cons 1021 ref subst appThm 1057 remove refl appThm sym 273 ref 224 ref 231 ref 568 ref 1054 remove 216 ref "Number.Natural.Bits.or" const 237 ref constTerm 1063 def 968 ref appTerm 969 ref appTerm 1064 def appTerm appTerm absTerm 1065 def 571 ref appTerm 1066 def betaConv 567 ref 6 ref 1065 ref appTerm 1067 def absTerm 1068 def 569 ref appTerm 1069 def betaConv nil 6 ref 1068 ref appTerm 1070 def axiom nil 43 ref 1070 remove nil cons cons 44 ref 1069 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1068 remove nil cons cons 951 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1067 remove nil cons cons 44 ref 1066 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1065 remove nil cons cons 973 ref cons nil cons cons 138 ref subst eqMp eqMp appThm nil 161 ref 1064 ref nil cons cons nil cons 1071 def nil cons cons 269 ref subst trans 1072 def appThm appThm nil 11 ref 1056 remove nil cons cons nil cons nil cons cons 223 ref subst 224 ref 274 remove 1055 ref refl 1032 remove appThm 1033 remove appThm 1037 remove 158 ref 144 ref 1055 remove 1038 remove appTerm 166 remove appTerm 1073 def appTerm 146 remove 1063 remove 497 ref appTerm 164 ref appTerm 1074 def appTerm 165 ref appTerm 1075 def appTerm 1076 def absTerm 1077 def 165 ref appTerm 1078 def betaConv 161 ref 170 ref 1077 ref appTerm 1079 def absTerm 1080 def 164 ref appTerm 1081 def betaConv 495 ref 170 ref 1080 ref appTerm 1082 def absTerm 1083 def 497 ref appTerm 1084 def betaConv 242 ref 495 ref 242 ref 161 ref 242 ref 158 ref 1076 remove assume sym 144 ref 1075 remove appTerm 1073 remove appTerm 1085 def assume sym deductAntisym absThm appThm absThm appThm absThm appThm nil 170 ref 495 ref 170 ref 161 ref 170 ref 158 ref 1085 remove absTerm appTerm absTerm appTerm absTerm appTerm axiom eqMp nil 43 ref 170 ref 1083 ref appTerm nil cons cons 44 ref 1084 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1083 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1082 remove nil cons cons 44 ref 1081 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1080 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1079 remove nil cons cons 44 ref 1078 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1077 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans appThm nil 160 ref 1071 remove cons 1086 def nil cons cons 282 remove subst trans appThm trans appThm nil 155 ref 216 ref 238 ref 1064 remove appTerm 37 ref appTerm appTerm nil cons cons nil cons nil cons cons 301 ref subst trans sym 79 ref eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 6 ref 1061 remove appTerm thm nil 110 ref 11 ref 170 ref 161 ref 212 ref "Data.Word.shiftLeft" const 1 ref 2 ref 215 ref nil cons cons opType 1087 def constTerm 1088 def 214 ref appTerm 164 ref appTerm 1089 def appTerm 213 ref 367 ref 371 ref 164 ref appTerm 1090 def appTerm 25 ref appTerm 1091 def appTerm 1092 def appTerm 1093 def absTerm 1094 def appTerm 1095 def absTerm 1096 def nil cons cons nil cons nil cons cons 330 ref subst 11 ref nil 74 ref 1095 remove nil cons cons nil cons nil cons cons 80 ref subst nil 177 ref 1094 remove nil cons cons nil cons nil cons cons 525 ref subst 161 ref nil 74 ref 1093 remove nil cons 1097 def cons nil cons nil cons cons 80 ref subst 140 ref 231 ref 345 ref 161 ref 212 ref 1088 ref 14 ref appTerm 164 ref appTerm appTerm 216 ref "Number.Natural.Bits.shiftLeft" const 237 ref constTerm 1098 def 148 ref appTerm 164 ref appTerm appTerm appTerm absTerm 1099 def 164 ref appTerm 1100 def betaConv 8 ref 170 ref 1099 ref appTerm 1101 def absTerm 1102 def 14 ref appTerm 1103 def betaConv nil 6 ref 1102 ref appTerm 1104 def axiom nil 43 ref 1104 remove nil cons cons 44 ref 1103 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1102 remove nil cons cons 156 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1101 remove nil cons cons 44 ref 1100 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1099 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp 1105 def subst 224 ref 1098 ref refl 350 ref appThm 164 ref refl 1106 def appThm nil 158 ref 179 ref cons 1107 def "j" 27 ref var 1108 def 159 ref cons 1109 def 348 ref cons 1110 def cons nil cons cons 158 ref 31 ref 1098 ref 239 ref 1108 ref varTerm 1111 def appTerm 1112 def appTerm 165 ref appTerm 1113 def appTerm 238 ref 1098 ref 164 ref appTerm 1114 def 165 ref appTerm appTerm "Number.Natural.+" const 237 ref constTerm 1115 def 1111 ref appTerm 165 ref appTerm 1116 def appTerm 1117 def appTerm 1118 def absTerm 1119 def 165 ref appTerm 1120 def betaConv 1108 ref 170 ref 1119 ref appTerm 1121 def absTerm 1122 def 1111 ref appTerm 1123 def betaConv 161 ref 170 ref 1122 ref appTerm 1124 def absTerm 1125 def 164 ref appTerm 1126 def betaConv 242 ref 161 ref 242 ref 1108 ref 242 ref 158 ref 1118 remove assume sym 31 ref 1117 remove appTerm 1113 remove appTerm 1127 def assume sym deductAntisym absThm appThm absThm appThm absThm appThm nil 170 ref 161 ref 170 ref 1108 ref 170 ref 158 ref 1127 remove absTerm appTerm absTerm appTerm absTerm appTerm axiom eqMp nil 43 ref 170 ref 1125 ref appTerm nil cons cons 44 ref 1126 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1125 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1124 remove nil cons cons 44 ref 1123 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1122 remove nil cons cons 178 ref 1111 ref nil cons cons nil cons 1128 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1121 remove nil cons cons 44 ref 1120 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1119 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans appThm trans appThm nil 161 ref 238 ref 1098 ref 218 ref appTerm 1129 def 164 ref appTerm 1130 def appTerm 1131 def 1115 ref 37 ref appTerm 164 ref appTerm 1132 def appTerm nil cons cons nil cons nil cons cons 269 ref subst nil 160 ref 1108 ref 1132 ref nil cons 1133 def cons 161 ref 1130 remove nil cons cons nil cons 1134 def cons cons nil cons cons 158 ref 31 ref 238 ref 1112 remove appTerm 165 ref appTerm appTerm 239 ref "Number.Natural.min" const 237 ref constTerm 1135 def 1111 ref appTerm 165 ref appTerm appTerm appTerm absTerm 1136 def 165 ref appTerm 1137 def betaConv 1108 ref 170 ref 1136 ref appTerm 1138 def absTerm 1139 def 1111 ref appTerm 1140 def betaConv 161 ref 170 ref 1139 ref appTerm 1141 def absTerm 1142 def 164 ref appTerm 1143 def betaConv nil 170 ref 1142 ref appTerm 1144 def axiom nil 43 ref 1144 remove nil cons cons 44 ref 1143 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1142 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1141 remove nil cons cons 44 ref 1140 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1139 remove nil cons cons 1128 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1138 remove nil cons cons 44 ref 1137 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1136 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp 1145 def subst trans trans appThm 231 ref nil 11 ref 1091 remove nil cons cons nil cons nil cons cons 223 ref subst 224 ref nil 642 ref 112 remove cons 654 ref 1090 remove nil cons cons nil cons cons nil cons cons 642 ref 31 ref 217 ref 367 remove 655 ref appTerm 645 ref appTerm appTerm appTerm 1115 ref 657 remove appTerm 1098 remove 651 remove appTerm 656 remove appTerm appTerm appTerm absTerm 1146 def 645 remove appTerm 1147 def betaConv 654 ref 41 ref 1146 ref appTerm 1148 def absTerm 1149 def 655 ref appTerm 1150 def betaConv nil 41 ref 1149 ref appTerm 1151 def axiom nil 43 ref 1151 remove nil cons cons 44 ref 1150 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 1149 remove nil cons cons 111 ref 655 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1148 remove nil cons cons 44 ref 1147 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 1146 remove nil cons cons 906 remove cons nil cons cons 138 ref subst eqMp eqMp subst 1115 ref refl 1152 def nil 1107 ref nil cons nil cons cons 1153 def 158 ref 31 ref 217 ref 371 ref 165 ref appTerm appTerm appTerm 226 ref appTerm absTerm 1154 def 165 ref appTerm 1155 def betaConv nil 170 ref 1154 ref appTerm 1156 def axiom nil 43 ref 1156 remove nil cons cons 44 ref 1155 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1154 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp subst appThm 1129 remove refl 401 remove 402 ref 161 ref 31 ref 701 ref 409 remove 164 ref appTerm appTerm appTerm 164 ref appTerm absTerm 1157 def 164 ref appTerm 1158 def betaConv 122 ref 170 ref 1157 ref appTerm 1159 def absTerm 1160 def 123 ref appTerm 1161 def betaConv nil 117 ref 1160 ref appTerm 1162 def axiom nil 43 ref 1162 remove nil cons cons 44 ref 1161 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 1160 remove nil cons cons 415 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1159 remove nil cons cons 44 ref 1158 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1157 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst subst appThm appThm nil 1134 remove nil cons cons 1163 def 161 ref 31 ref 1115 ref 226 ref appTerm 164 ref appTerm appTerm 164 ref appTerm absTerm 1164 def 164 ref appTerm 1165 def betaConv nil 170 ref 1164 ref appTerm 1166 def axiom nil 43 ref 1166 remove nil cons cons 44 ref 1165 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1164 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans trans appThm trans appThm 1163 remove 269 ref subst trans appThm sym 140 ref 1131 ref refl 1167 def nil 385 ref 495 ref 1133 ref cons nil cons cons nil cons cons 161 ref 31 ref 1135 ref 497 ref appTerm 164 ref appTerm appTerm 1168 def 1135 remove 164 ref appTerm 497 ref appTerm appTerm absTerm 1169 def 164 ref appTerm 1170 def betaConv 495 ref 170 ref 1169 ref appTerm 1171 def absTerm 1172 def 497 ref appTerm 1173 def betaConv nil 170 ref 1172 ref appTerm 1174 def axiom nil 43 ref 1174 remove nil cons cons 44 ref 1173 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1172 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1171 remove nil cons cons 44 ref 1170 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1169 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst appThm appThm 1131 remove 37 ref appTerm refl appThm sym 1167 remove nil 161 ref 1133 ref cons 495 ref 159 ref cons nil cons 1175 def cons nil cons cons 161 ref 1168 remove 359 ref 1 ref 3 ref 237 ref nil cons cons opType constTerm 1176 def 499 ref appTerm 497 ref appTerm 164 ref appTerm appTerm absTerm 1177 def 164 ref appTerm 1178 def betaConv 495 ref 170 ref 1177 ref appTerm 1179 def absTerm 1180 def 497 ref appTerm 1181 def betaConv nil 170 ref 1180 ref appTerm 1182 def axiom nil 43 ref 1182 remove nil cons cons 44 ref 1181 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1180 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1179 remove nil cons cons 44 ref 1178 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1177 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst 1176 ref refl nil 1175 ref nil cons cons nil 74 ref 498 ref 1115 ref 497 ref appTerm 164 ref appTerm appTerm 1183 def nil cons cons nil cons nil cons cons 80 ref subst 161 ref 1183 remove absTerm 1184 def 164 ref appTerm 1185 def betaConv 495 ref 170 ref 1184 ref appTerm 1186 def absTerm 1187 def 497 ref appTerm 1188 def betaConv nil 170 ref 1187 ref appTerm 1189 def axiom nil 43 ref 1189 remove nil cons cons 44 ref 1188 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1187 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1186 remove nil cons cons 44 ref 1185 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1184 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp eqMp subst appThm 184 remove appThm 1132 remove refl 1190 def appThm nil 883 ref 1133 ref cons 884 ref 159 ref cons nil cons cons nil cons cons 187 ref 445 ref subst 1191 def subst trans trans 1192 def appThm eqMp eqMp nil 43 ref 31 ref 147 ref 1089 ref appTerm appTerm 147 ref 1092 ref appTerm appTerm nil cons cons 44 ref 1097 remove cons nil cons cons nil cons cons 108 ref subst proveHyp nil 950 ref 1092 remove nil cons cons 155 ref 1089 remove nil cons cons nil cons cons nil cons cons 950 ref 45 ref 31 ref 287 remove appTerm 954 remove appTerm appTerm 1017 remove 953 ref appTerm appTerm absTerm 1193 def 953 remove appTerm 1194 def betaConv 155 ref 6 ref 1193 ref appTerm 1195 def absTerm 1196 def 286 ref appTerm 1197 def betaConv nil 6 ref 1196 ref appTerm 1198 def axiom nil 43 ref 1198 remove nil cons cons 44 ref 1197 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1196 remove nil cons cons 291 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1195 remove nil cons cons 44 ref 1194 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1193 remove nil cons cons 961 remove cons nil cons cons 138 ref subst eqMp eqMp 1199 def subst eqMp eqMp absThm eqMp eqMp absThm eqMp nil 41 ref 1096 remove appTerm thm nil 177 ref 158 ref 6 ref 8 ref 22 ref "Data.Word.bit" const 1 ref 2 ref 29 ref cons opType constTerm 1200 def "Data.Word.not" const 1004 remove constTerm 14 ref appTerm 1201 def appTerm 165 ref appTerm appTerm 1202 def 50 ref 309 ref 165 ref appTerm 1203 def 37 ref appTerm 1204 def appTerm 1205 def 724 ref 1200 ref 14 ref appTerm 1206 def 165 ref appTerm appTerm appTerm appTerm 1207 def absTerm 1208 def appTerm 1209 def absTerm 1210 def nil cons cons nil cons nil cons cons 525 ref subst 158 ref nil 74 ref 1209 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 1208 remove nil cons cons nil cons nil cons cons 579 ref subst 8 ref nil 74 ref 1207 remove nil cons cons nil cons nil cons cons 80 ref subst 1202 remove refl 1205 ref refl 1211 def 731 ref 1200 ref refl 1212 def 589 ref appThm 165 ref refl 1213 def appThm appThm appThm appThm sym 89 ref 1212 ref 8 ref 212 ref 1201 remove appTerm 213 ref "Data.List.map" const 1214 def 1 ref 20 ref 360 remove cons opType constTerm 724 ref appTerm 15 ref appTerm 1215 def appTerm appTerm absTerm 1216 def 14 ref appTerm 1217 def betaConv nil 6 ref 1216 ref appTerm 1218 def axiom nil 43 ref 1218 remove nil cons cons 44 ref 1217 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1216 remove nil cons cons 156 ref cons nil cons cons 138 ref subst eqMp eqMp appThm 1213 ref appThm nil 161 ref 181 ref cons 1219 def 11 ref 1215 ref nil cons cons nil cons cons nil cons cons 345 ref 161 ref 22 ref 1206 remove 164 ref appTerm appTerm "Number.Natural.Bits.bit" const 30 remove constTerm 1220 def 148 ref appTerm 164 ref appTerm appTerm absTerm 1221 def 164 ref appTerm 1222 def betaConv 8 ref 170 ref 1221 ref appTerm 1223 def absTerm 1224 def 14 ref appTerm 1225 def betaConv nil 6 ref 1224 ref appTerm 1226 def axiom nil 43 ref 1226 remove nil cons cons 44 ref 1225 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1224 remove nil cons cons 156 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1223 remove nil cons cons 44 ref 1222 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1221 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp 1227 def subst 1220 ref refl 1228 def 350 remove appThm 1106 ref appThm nil "i" 27 ref var 1229 def 179 remove cons 1230 def 351 remove cons nil cons cons 158 ref 22 ref 1220 ref 256 remove appTerm 1229 ref varTerm 1231 def appTerm appTerm 50 ref 309 ref 1231 ref appTerm 1232 def 165 ref appTerm appTerm 1220 ref 164 ref appTerm 1231 ref appTerm 1233 def appTerm appTerm absTerm 1234 def 165 ref appTerm 1235 def betaConv 1229 ref 170 ref 1234 ref appTerm 1236 def absTerm 1237 def 1231 ref appTerm 1238 def betaConv 161 ref 170 ref 1237 ref appTerm 1239 def absTerm 1240 def 164 ref appTerm 1241 def betaConv nil 170 ref 1240 ref appTerm 1242 def axiom nil 43 ref 1242 remove nil cons cons 44 ref 1241 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1240 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1239 remove nil cons cons 44 ref 1238 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1237 remove nil cons cons 178 ref 1231 ref nil cons 1243 def cons nil cons 1244 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1236 remove nil cons cons 44 ref 1235 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1234 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp 1245 def subst 50 ref 310 ref 37 ref appTerm appTerm 1246 def refl nil 1230 remove nil cons nil cons cons 1229 ref 22 ref 1220 ref 218 ref appTerm 1231 ref appTerm appTerm 50 ref 1232 ref 36 ref appTerm appTerm "Data.List.nth" const 1247 def 1 ref 10 ref 29 remove cons opType constTerm 1248 def 25 ref appTerm 1249 def 1231 ref appTerm appTerm appTerm absTerm 1250 def 1231 ref appTerm 1251 def betaConv 11 ref 170 ref 1250 ref appTerm 1252 def absTerm 1253 def 25 ref appTerm 1254 def betaConv nil 41 ref 1253 ref appTerm 1255 def axiom nil 43 ref 1255 remove nil cons cons 44 ref 1254 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 1253 remove nil cons cons 113 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1252 remove nil cons cons 44 ref 1251 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1250 remove nil cons cons 1244 ref cons nil cons cons 138 ref subst eqMp eqMp subst appThm trans trans trans 1256 def subst 1211 ref 455 ref 1203 ref refl 1257 def nil 16 remove "f" 20 remove var 724 ref nil cons cons nil cons cons 1258 def nil cons cons 202 remove "B" 4 ref cons nil cons cons 186 ref cons 1259 def 416 ref 31 ref 32 remove 1 ref 9 remove 668 ref nil cons 1260 def opType 1261 def 33 ref cons opType constTerm 1214 remove 1 ref 1 ref 114 ref 1260 ref cons opType 1262 def 1 ref 404 ref 1261 ref nil cons cons opType nil cons cons opType constTerm "f" 1262 ref var 1263 def varTerm 1264 def appTerm 418 ref appTerm 1265 def appTerm appTerm 704 ref appTerm absTerm 1266 def 418 ref appTerm 1267 def betaConv 1263 ref 422 ref 1266 ref appTerm 1268 def absTerm 1269 def 1264 ref appTerm 1270 def betaConv nil 0 ref 1 ref 1 ref 1262 ref 4 ref cons opType 1271 def 4 remove cons opType constTerm 1272 def 1269 ref appTerm 1273 def axiom nil 43 ref 1273 remove nil cons cons 44 ref 1270 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp "A" 1262 ref nil cons cons nil cons 1274 def "P" 1271 remove var 1275 def 1269 remove nil cons cons "x" 1262 remove var 1264 ref nil cons cons nil cons 1276 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1268 remove nil cons cons 44 ref 1267 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 424 ref 425 ref 1266 remove nil cons cons 427 ref cons nil cons cons 138 ref subst eqMp eqMp subst subst 183 ref trans appThm appThm 1248 ref 1215 remove appTerm 165 ref appTerm 1277 def refl 1278 def appThm appThm trans trans appThm 1211 ref 731 ref nil 1219 ref 17 remove cons nil cons cons 1256 ref subst 1211 ref 455 ref 1257 remove 183 remove appThm 1279 def appThm 1248 ref 15 remove appTerm 165 ref appTerm 1280 def refl 1281 def appThm appThm trans appThm appThm appThm sym nil 43 ref 724 ref 1204 ref appTerm nil cons 1282 def cons 1283 def 44 ref 22 ref 1205 ref 1205 ref 1277 ref appTerm appTerm appTerm 1205 ref 724 ref 1205 ref 1205 ref 1280 ref appTerm appTerm appTerm appTerm appTerm nil cons 1284 def cons nil cons 1285 def cons nil cons cons 1286 def 61 ref subst 1286 remove 127 ref subst 89 ref 455 ref nil 1283 remove 44 ref 22 ref 1204 ref appTerm 370 ref appTerm nil cons cons nil cons cons nil cons cons 108 ref subst nil 86 ref 1204 ref nil cons 1287 def cons 1288 def nil cons nil cons cons 807 ref subst eqMp appThm 1289 def 1289 ref 1278 ref appThm nil 74 ref 1277 ref nil cons cons nil cons nil cons cons 1290 def 74 ref 22 ref 50 ref 370 ref appTerm 76 ref appTerm appTerm 370 ref appTerm absTerm 1291 def 76 ref appTerm 1292 def betaConv nil 200 ref 1291 ref appTerm 1293 def axiom nil 43 ref 1293 remove nil cons cons 44 ref 1292 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1291 remove nil cons cons 206 ref cons nil cons cons 138 ref subst eqMp eqMp 1294 def subst trans appThm nil 74 ref 399 remove cons nil cons nil cons cons 1295 def 1294 ref subst 1296 def trans appThm 1289 ref 731 ref 1289 ref 1289 remove 1281 ref appThm nil 74 ref 1280 ref nil cons cons nil cons nil cons cons 1297 def 1294 ref subst trans appThm 1296 remove trans appThm nil 22 ref 724 ref 370 ref appTerm appTerm 66 ref appTerm axiom 1298 def trans appThm 196 ref 1294 remove subst trans appThm 1295 remove 74 ref 22 ref 804 remove 76 ref appTerm appTerm 724 ref 76 ref appTerm 1299 def appTerm absTerm 1300 def 76 ref appTerm 1301 def betaConv nil 200 ref 1300 ref appTerm 1302 def axiom nil 43 ref 1302 remove nil cons cons 44 ref 1301 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1300 remove nil cons cons 206 ref cons nil cons cons 138 ref subst eqMp eqMp subst 1298 ref trans trans sym 79 ref eqMp eqMp nil 86 ref 1282 ref cons 87 ref 1284 ref cons nil cons 1303 def cons nil cons cons 101 ref subst deductAntisym eqMp nil 43 ref 1287 ref cons 1304 def 1285 remove cons nil cons cons 1305 def 61 ref subst 1305 remove 127 ref subst 89 ref 455 ref nil 74 ref 1287 ref cons nil cons nil cons cons 80 ref subst 1204 ref assume eqMp 1306 def appThm 1307 def 1307 ref 1278 remove appThm 1290 remove 470 ref subst 1308 def trans appThm 1308 remove trans appThm 1307 ref 731 ref 1307 ref 1307 remove 1281 remove appThm 1297 remove 470 ref subst 1309 def trans appThm 1309 remove trans appThm appThm nil 74 ref 724 ref 1280 remove appTerm 1310 def nil cons cons nil cons nil cons cons 470 ref subst trans appThm sym 1279 remove 1306 remove trans sym 79 ref eqMp nil 43 ref 1203 remove 305 remove appTerm nil cons cons 44 ref 22 ref 1277 remove appTerm 1310 remove appTerm nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp nil 1229 ref 181 remove cons 1311 def 1258 remove cons nil cons cons 1259 remove 1229 ref 45 ref 1232 ref 704 ref appTerm appTerm 19 remove 1 ref 668 ref 670 remove cons opType constTerm 1312 def 1247 ref 1 ref 1261 remove 1 ref 27 ref 1260 ref cons opType nil cons cons opType constTerm 1265 remove appTerm 1231 ref appTerm appTerm 1264 ref 1247 remove 1 ref 404 ref 1 ref 27 ref 403 remove cons opType nil cons cons opType constTerm 1313 def 418 ref appTerm 1231 ref appTerm appTerm appTerm appTerm absTerm 1314 def 1231 ref appTerm 1315 def betaConv 416 ref 170 ref 1314 ref appTerm 1316 def absTerm 1317 def 418 ref appTerm 1318 def betaConv 1263 ref 422 ref 1317 ref appTerm 1319 def absTerm 1320 def 1264 ref appTerm 1321 def betaConv nil 1272 ref 1320 ref appTerm 1322 def axiom nil 43 ref 1322 remove nil cons cons 44 ref 1321 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 1274 ref 1275 ref 1320 remove nil cons cons 1276 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1319 remove nil cons cons 44 ref 1318 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 424 ref 425 ref 1317 remove nil cons cons 427 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1316 remove nil cons cons 44 ref 1315 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1314 remove nil cons cons 1244 ref cons nil cons cons 138 ref subst eqMp eqMp subst subst eqMp eqMp eqMp nil 1288 ref 1303 remove cons nil cons cons 101 ref subst deductAntisym eqMp 74 ref 733 remove 1299 ref appTerm absTerm 1323 def 1204 remove appTerm 1324 def betaConv nil 200 ref 1323 ref appTerm 1325 def axiom 1326 def nil 43 ref 1325 remove nil cons cons 1327 def 44 ref 1324 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1323 ref nil cons cons 1328 def 205 ref 1287 ref cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 1288 remove 87 ref 1282 remove cons "R" 3 ref var 1329 def 1284 remove cons nil cons cons cons nil cons cons nil 43 ref 45 ref 92 ref appTerm 1330 def 1329 ref varTerm 1331 def appTerm 1332 def nil cons cons 44 ref 1331 ref nil cons 1333 def cons nil cons cons nil cons cons 108 ref subst nil 43 ref 799 ref 1331 ref appTerm nil cons cons 44 ref 45 ref 1332 remove appTerm 1331 ref appTerm nil cons cons nil cons cons nil cons cons 108 ref subst "r" 3 ref var 1334 def 45 ref 799 remove 1334 ref varTerm 1335 def appTerm appTerm 1336 def 45 ref 1330 remove 1335 ref appTerm appTerm 1335 ref appTerm appTerm absTerm 1337 def 1331 remove appTerm 1338 def betaConv 22 ref 722 ref 90 ref appTerm 1339 def 92 ref appTerm 1340 def appTerm refl 44 ref 200 ref 1334 ref 1336 remove 45 ref 339 remove 1335 ref appTerm appTerm 1335 ref appTerm 1341 def appTerm absTerm appTerm absTerm 92 remove appTerm betaConv appThm 70 remove 1339 remove appTerm refl 43 ref 44 ref 200 ref 1334 ref 45 ref 47 remove 1335 ref appTerm appTerm 1341 remove appTerm absTerm appTerm absTerm absTerm 1342 def 90 remove appTerm betaConv appThm nil 58 remove 722 ref appTerm 1342 remove appTerm axiom 99 remove appThm eqMp 95 remove appThm eqMp 1340 remove assume eqMp nil 43 ref 200 ref 1337 ref appTerm nil cons cons 44 ref 1338 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1337 remove nil cons cons 205 ref 1333 remove cons nil cons cons nil cons cons 138 ref subst eqMp eqMp eqMp eqMp 1343 def subst proveHyp proveHyp proveHyp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 170 ref 1210 remove appTerm thm nil 177 ref 158 ref 6 ref 567 ref 6 ref 568 ref 22 ref 1200 ref 1006 remove appTerm 165 ref appTerm appTerm 1344 def 50 ref 1200 ref 569 remove appTerm 1345 def 165 ref appTerm 1346 def appTerm 1200 ref 571 remove appTerm 1347 def 165 ref appTerm 1348 def appTerm appTerm 1349 def absTerm 1350 def appTerm 1351 def absTerm 1352 def appTerm 1353 def absTerm 1354 def nil cons cons nil cons nil cons cons 525 ref subst 158 ref nil 74 ref 1353 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 1352 remove nil cons cons nil cons nil cons cons 579 ref subst 567 ref nil 74 ref 1351 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 1350 remove nil cons cons nil cons nil cons cons 579 ref subst 568 ref nil 74 ref 1349 remove nil cons cons nil cons nil cons cons 80 ref subst 1344 remove refl 455 ref 1212 ref nil 951 remove nil cons cons 1021 ref subst appThm 1213 ref appThm 1355 def appThm 1348 ref refl 1356 def appThm appThm sym 89 ref nil 1219 ref 8 ref 1016 remove cons nil cons cons nil cons cons 1227 ref subst 1228 ref 1031 remove appThm 1213 ref appThm nil 1311 ref 1052 remove cons nil cons cons 1245 ref subst 1211 ref nil 1311 ref 1034 ref 1036 remove cons cons nil cons cons 1357 def 1229 ref 22 ref 1220 ref 1040 remove appTerm 1231 ref appTerm appTerm 50 ref 1220 ref 497 ref appTerm 1231 ref appTerm 1358 def appTerm 1233 ref appTerm appTerm absTerm 1359 def 1231 ref appTerm 1360 def betaConv 161 ref 170 ref 1359 ref appTerm 1361 def absTerm 1362 def 164 ref appTerm 1363 def betaConv 495 ref 170 ref 1362 ref appTerm 1364 def absTerm 1365 def 497 ref appTerm 1366 def betaConv nil 170 ref 1365 ref appTerm 1367 def axiom nil 43 ref 1367 remove nil cons cons 44 ref 1366 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1365 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1364 remove nil cons cons 44 ref 1363 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1362 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1361 remove nil cons cons 44 ref 1360 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1359 remove nil cons cons 1244 ref cons nil cons cons 138 ref subst eqMp eqMp subst appThm nil "t3" 3 ref var 1368 def 1220 ref 969 ref appTerm 165 ref appTerm 1369 def nil cons 1370 def cons 974 ref 1220 ref 968 ref appTerm 165 ref appTerm 1371 def nil cons 1372 def cons 975 ref 1287 remove cons nil cons cons cons nil cons cons 1368 ref 22 ref 50 ref 975 ref varTerm 1373 def appTerm 1374 def 50 ref 974 ref varTerm 1375 def appTerm 1368 ref varTerm 1376 def appTerm appTerm 1377 def appTerm 50 ref 1374 remove 1375 ref appTerm appTerm 1376 ref appTerm 1378 def appTerm 1379 def absTerm 1380 def 1376 ref appTerm 1381 def betaConv 974 ref 200 ref 1380 ref appTerm 1382 def absTerm 1383 def 1375 ref appTerm 1384 def betaConv 975 ref 200 ref 1383 ref appTerm 1385 def absTerm 1386 def 1373 ref appTerm 1387 def betaConv 664 ref 975 ref 664 ref 974 ref 664 ref 1368 ref 1379 remove assume sym 22 ref 1378 remove appTerm 1377 remove appTerm 1388 def assume sym deductAntisym absThm appThm absThm appThm absThm appThm nil 200 ref 975 remove 200 ref 974 remove 200 ref 1368 remove 1388 remove absTerm appTerm absTerm appTerm absTerm appTerm axiom eqMp nil 43 ref 200 ref 1386 ref appTerm nil cons cons 44 ref 1387 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1386 remove nil cons cons 205 ref 1373 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1385 remove nil cons cons 44 ref 1384 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1383 remove nil cons cons 205 ref 1375 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1382 remove nil cons cons 44 ref 1381 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1380 remove nil cons cons 205 ref 1376 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp subst trans trans trans trans appThm 455 ref nil 1219 ref 8 ref 216 ref 968 remove appTerm 1389 def nil cons cons nil cons cons nil cons cons 1227 ref subst 1228 ref nil 161 ref 1035 remove cons nil cons 1390 def nil cons cons 269 ref subst appThm 1213 ref appThm nil 1311 ref 160 ref 1390 remove cons cons nil cons cons 1245 ref subst trans trans 1391 def appThm nil 1219 ref 592 remove cons nil cons cons 1227 ref subst appThm appThm nil 205 ref 50 ref 1205 ref 1371 remove appTerm 1392 def appTerm 1369 ref appTerm nil cons cons nil cons nil cons cons 737 ref subst trans sym 79 ref eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 170 ref 1354 remove appTerm thm nil 177 ref 158 ref 6 ref 567 ref 6 ref 568 ref 22 ref 1200 ref 1053 remove appTerm 165 ref appTerm appTerm 1393 def 722 ref 1346 remove appTerm 1348 remove appTerm appTerm 1394 def absTerm 1395 def appTerm 1396 def absTerm 1397 def appTerm 1398 def absTerm 1399 def nil cons cons nil cons nil cons cons 525 ref subst 158 ref nil 74 ref 1398 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 1397 remove nil cons cons nil cons nil cons cons 579 ref subst 567 ref nil 74 ref 1396 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 1395 remove nil cons cons nil cons nil cons cons 579 ref subst 568 ref nil 74 ref 1394 remove nil cons cons nil cons nil cons cons 80 ref subst 1393 remove refl 1400 def 722 ref refl 1401 def 1355 remove appThm 1356 remove appThm appThm sym 1400 remove 722 ref 1200 ref 1389 remove appTerm 165 ref appTerm appTerm refl 1212 ref nil 973 remove nil cons cons 1021 remove subst appThm 1213 ref appThm appThm appThm sym 89 ref nil 1219 ref 8 ref 1062 remove cons nil cons cons nil cons cons 1227 ref subst 1228 ref 1072 remove appThm 1213 ref appThm nil 1311 ref 1086 remove cons nil cons cons 1245 ref subst 1211 remove 1357 remove 1229 ref 22 ref 1220 remove 1074 remove appTerm 1231 ref appTerm appTerm 722 ref 1358 remove appTerm 1233 remove appTerm appTerm absTerm 1402 def 1231 ref appTerm 1403 def betaConv 161 ref 170 ref 1402 ref appTerm 1404 def absTerm 1405 def 164 ref appTerm 1406 def betaConv 495 ref 170 ref 1405 ref appTerm 1407 def absTerm 1408 def 497 ref appTerm 1409 def betaConv nil 170 ref 1408 ref appTerm 1410 def axiom nil 43 ref 1410 remove nil cons cons 44 ref 1409 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1408 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1407 remove nil cons cons 44 ref 1406 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1405 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1404 remove nil cons cons 44 ref 1403 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1402 remove nil cons cons 1244 ref cons nil cons cons 138 ref subst eqMp eqMp subst appThm nil 1334 ref 1370 remove cons 44 ref 1372 remove cons 1304 remove nil cons cons cons nil cons cons 1334 remove 22 ref 51 ref 723 remove 1335 ref appTerm appTerm appTerm 722 ref 52 remove appTerm 51 remove 1335 ref appTerm appTerm appTerm absTerm 1411 def 1335 ref appTerm 1412 def betaConv 44 ref 200 ref 1411 ref appTerm 1413 def absTerm 1414 def 48 remove appTerm 1415 def betaConv 43 ref 200 ref 1414 ref appTerm 1416 def absTerm 1417 def 46 remove appTerm 1418 def betaConv nil 200 ref 1417 ref appTerm 1419 def axiom nil 43 ref 1419 remove nil cons cons 44 ref 1418 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1417 remove nil cons cons 205 ref 75 remove cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1416 remove nil cons cons 44 ref 1415 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1414 remove nil cons cons 720 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1413 remove nil cons cons 44 ref 1412 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1411 remove nil cons cons 205 ref 1335 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp subst trans trans trans trans appThm 1401 remove 1391 remove appThm nil 1219 remove 8 ref 216 ref 969 remove appTerm nil cons cons nil cons cons nil cons cons 1227 remove subst 1228 remove nil 1034 remove nil cons 1420 def nil cons cons 269 ref subst appThm 1213 remove appThm nil 1311 remove 160 remove 1420 remove cons cons nil cons cons 1245 remove subst trans trans appThm appThm nil 205 ref 722 ref 1392 remove appTerm 1205 remove 1369 remove appTerm appTerm nil cons cons nil cons nil cons cons 737 ref subst trans sym 79 ref eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 170 ref 1399 remove appTerm thm 970 remove nil 971 remove thm nil 154 ref 567 ref 6 ref 568 ref 45 ref 170 ref 1229 ref 45 ref 1232 ref 37 ref appTerm 1421 def appTerm 1422 def 22 ref 1345 remove 1231 ref appTerm appTerm 1347 remove 1231 ref appTerm appTerm appTerm absTerm appTerm appTerm 574 ref appTerm 1423 def absTerm 1424 def appTerm 1425 def absTerm 1426 def nil cons cons nil cons nil cons cons 579 ref subst 567 remove nil 74 ref 1425 remove nil cons cons nil cons nil cons cons 80 ref subst nil 154 ref 1424 remove nil cons cons nil cons nil cons cons 579 remove subst 568 remove nil 74 ref 1423 remove nil cons cons nil cons nil cons cons 80 ref subst 689 ref 242 ref 1229 ref 1422 ref refl 1427 def 89 ref 1212 ref 590 remove appThm 1231 ref refl 1428 def appThm appThm 1212 remove 594 remove appThm 1428 remove appThm appThm appThm absThm appThm appThm 574 remove refl 1429 def appThm sym 689 ref 242 ref 1229 ref 1427 remove 89 ref nil 161 ref 1243 remove cons 1430 def 11 ref 917 ref cons nil cons cons nil cons cons 1256 ref subst appThm nil 1430 remove 11 ref 918 ref cons nil cons cons nil cons cons 1256 ref subst appThm appThm absThm appThm appThm 1429 remove appThm sym nil 43 ref 170 ref 1229 ref 1422 ref 22 ref 50 ref 1421 ref appTerm 1431 def 50 ref 1232 ref 643 remove appTerm 1432 def appTerm 1248 ref 570 remove appTerm 1231 ref appTerm 1433 def appTerm appTerm appTerm 1431 remove 50 ref 1232 ref 919 remove appTerm appTerm 1248 remove 572 remove appTerm 1231 ref appTerm 1434 def appTerm appTerm appTerm appTerm 1435 def absTerm 1436 def appTerm nil cons 1437 def cons 1438 def 582 remove cons nil cons cons 1439 def 61 ref subst 1439 remove 127 ref subst 455 ref 927 remove appThm 242 ref 1229 ref 689 ref 1232 ref refl 1440 def 925 remove appThm 1441 def appThm 22 ref 1433 ref appTerm 1434 ref appTerm 1442 def refl 1443 def appThm absThm appThm appThm nil 74 ref 170 ref 1229 ref 1422 remove 1442 ref appTerm 1444 def absTerm 1445 def appTerm nil cons cons nil cons nil cons cons 470 ref subst trans sym nil 177 ref 1445 remove nil cons cons nil cons nil cons cons 525 ref subst 1229 ref nil 74 ref 1444 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 1421 ref nil cons 1446 def cons 44 ref 1442 ref nil cons 1447 def cons nil cons 1448 def cons nil cons cons 1449 def 61 ref subst 1449 remove 127 ref subst 1436 ref 1231 ref appTerm 1450 def betaConv nil 1438 remove 44 ref 1450 remove nil cons cons nil cons cons nil cons cons 108 ref subst 176 ref 177 ref 1436 remove nil cons cons 1244 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1435 remove nil cons cons 1448 remove cons nil cons cons 108 ref subst proveHyp 689 ref 689 ref nil 74 ref 1446 ref cons nil cons nil cons cons 80 ref subst 1421 remove assume eqMp 1451 def appThm 89 ref 455 ref 1451 ref appThm 1452 def 455 ref 1441 remove 1451 ref trans appThm 1433 ref refl appThm nil 74 ref 1433 remove nil cons cons nil cons nil cons cons 470 ref subst 1453 def trans appThm 1453 remove trans appThm 1452 remove 455 ref 1440 remove 926 remove appThm 1451 remove trans appThm 1434 ref refl appThm nil 74 ref 1434 remove nil cons cons nil cons nil cons cons 470 remove subst 1454 def trans appThm 1454 remove trans appThm appThm nil 74 ref 1447 ref cons nil cons nil cons cons 1455 def 932 ref subst trans appThm 1443 remove appThm 1455 remove 989 ref subst trans sym 79 ref eqMp eqMp eqMp nil 86 ref 1446 remove cons 87 ref 1447 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 43 ref 50 ref 920 remove appTerm 170 ref 1229 ref 45 ref 1432 remove appTerm 1442 remove appTerm absTerm appTerm appTerm nil cons cons 600 remove cons nil cons cons 108 ref subst proveHyp nil 642 remove 918 remove cons 654 remove 917 remove cons nil cons cons nil cons cons 402 ref "l2" 404 ref var 1456 def 45 ref 50 ref 31 ref 701 ref "l1" 404 remove var 1457 def varTerm 1458 def appTerm 1459 def appTerm 701 ref 1456 remove varTerm 1460 def appTerm appTerm appTerm 170 ref 1229 remove 45 ref 1232 remove 1459 remove appTerm appTerm 189 remove 1313 ref 1458 ref appTerm 1231 ref appTerm appTerm 1313 remove 1460 ref appTerm 1231 remove appTerm appTerm appTerm absTerm appTerm appTerm appTerm 407 ref 1458 ref appTerm 1460 ref appTerm appTerm absTerm 1461 def 1460 ref appTerm 1462 def betaConv 1457 remove 422 ref 1461 ref appTerm 1463 def absTerm 1464 def 1458 ref appTerm 1465 def betaConv nil 422 ref 1464 ref appTerm 1466 def axiom nil 43 ref 1466 remove nil cons cons 44 ref 1465 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 424 ref 425 ref 1464 remove nil cons cons 426 ref 1458 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1463 remove nil cons cons 44 ref 1462 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 424 ref 425 ref 1461 remove nil cons cons 426 remove 1460 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp subst subst eqMp 583 remove 108 ref subst proveHyp 597 remove eqMp eqMp nil 86 ref 1437 remove cons 596 remove cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 6 ref 1426 remove appTerm thm 665 ref 11 ref 242 ref 161 ref 89 ref 1256 remove appThm 1246 remove 50 ref 310 ref 36 ref appTerm appTerm 1249 remove 164 ref appTerm appTerm appTerm 1467 def refl appThm nil 205 ref 1467 ref nil cons cons nil cons nil cons cons 737 remove subst trans absThm appThm 266 remove trans absThm appThm 196 remove 328 ref 207 remove subst subst 1468 def trans sym 79 ref eqMp nil 41 ref 11 ref 170 ref 161 ref 22 ref 1200 remove 214 ref appTerm 164 ref appTerm appTerm 1467 remove appTerm absTerm appTerm absTerm appTerm thm 915 remove nil 916 remove thm 665 ref 11 ref 144 remove refl 382 ref appThm 363 remove 364 ref 37 ref appTerm 1469 def appTerm 368 remove 371 remove 395 remove 36 ref appTerm appTerm appTerm 1470 def appTerm 428 ref appTerm 1471 def refl appThm nil 111 ref 1471 ref nil cons cons nil cons nil cons cons 328 ref 191 remove subst subst trans absThm appThm 1468 remove trans sym 79 ref eqMp nil 41 ref 11 ref 324 remove 1471 ref appTerm absTerm appTerm thm nil 204 ref 739 ref 41 ref 740 ref 212 ref 213 ref 752 ref appTerm appTerm 359 ref 1 ref 3 ref 1005 ref nil cons cons opType constTerm 1472 def 751 ref appTerm 1473 def "Data.Word.+" const 1005 ref constTerm 1474 def 216 ref 249 ref appTerm appTerm 1475 def 1088 remove 213 ref 741 remove appTerm 1476 def appTerm 249 ref appTerm 1477 def appTerm appTerm 1477 remove appTerm appTerm 1478 def absTerm 1479 def appTerm 1480 def absTerm 1481 def nil cons cons nil cons nil cons cons 483 remove subst 739 ref nil 74 ref 1480 remove nil cons cons nil cons nil cons cons 80 ref subst nil 110 ref 1479 remove nil cons cons nil cons nil cons cons 330 ref subst 740 remove nil 74 ref 1478 remove nil cons cons nil cons nil cons cons 80 ref subst 273 ref nil 11 ref 752 remove nil cons cons nil cons nil cons cons 223 ref subst 224 ref 882 remove nil "t" 27 ref var 1482 def 885 ref cons nil cons nil cons cons 1482 ref 31 ref 874 remove 1482 remove varTerm 1483 def appTerm appTerm 1115 ref "Number.Natural.fromBool" const 1 ref 3 ref 33 remove cons opType constTerm 1484 def 751 ref appTerm appTerm "Number.Natural.*" const 237 ref constTerm 1485 def 250 ref appTerm 1486 def 1483 ref appTerm appTerm appTerm absTerm 1487 def 1483 ref appTerm 1488 def betaConv 739 remove 170 ref 1487 ref appTerm 1489 def absTerm 1490 def 751 ref appTerm 1491 def betaConv nil 200 ref 1490 ref appTerm 1492 def axiom nil 43 ref 1492 remove nil cons cons 44 ref 1491 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1490 remove nil cons cons 881 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1489 remove nil cons cons 44 ref 1488 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1487 remove nil cons cons 178 ref 1483 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp subst trans 1152 remove nil "b" 3 ref var 1493 def 849 remove cons nil cons nil cons cons 1493 ref 31 ref 1484 remove 1493 ref varTerm 1494 def appTerm appTerm 1176 ref 1494 ref appTerm 249 ref appTerm 226 ref appTerm appTerm absTerm 1495 def 1494 ref appTerm 1496 def betaConv nil 200 ref 1495 ref appTerm 1497 def axiom nil 43 ref 1497 remove nil cons cons 44 ref 1496 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1495 remove nil cons cons 205 ref 1494 ref nil cons cons nil cons 1498 def cons nil cons cons 138 ref subst eqMp eqMp subst appThm 1486 ref 744 ref appTerm 1499 def refl appThm trans appThm nil "y1" 27 ref var 1500 def 1499 remove nil cons cons "x1" 27 ref var 1501 def 1176 ref 751 ref appTerm 249 ref appTerm 226 ref appTerm 1502 def nil cons cons nil cons cons nil cons cons 1500 ref 212 ref 216 ref 1115 remove 1501 ref varTerm 1503 def appTerm 1500 ref varTerm 1504 def appTerm appTerm appTerm 1474 ref 216 ref 1503 ref appTerm 1505 def appTerm 216 ref 1504 ref appTerm 1506 def appTerm appTerm absTerm 1507 def 1504 ref appTerm 1508 def betaConv 1501 ref 170 ref 1507 ref appTerm 1509 def absTerm 1510 def 1503 ref appTerm 1511 def betaConv nil 170 ref 1510 ref appTerm 1512 def axiom nil 43 ref 1512 remove nil cons cons 44 ref 1511 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1510 remove nil cons cons 178 ref 1503 ref nil cons cons nil cons 1513 def cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1509 remove nil cons cons 44 ref 1508 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1507 remove nil cons cons 178 ref 1504 ref nil cons cons nil cons 1514 def cons nil cons cons 138 ref subst eqMp eqMp subst 1474 ref 216 ref 1502 remove appTerm appTerm 1515 def refl nil 1500 ref 885 remove cons 1501 ref 250 ref nil cons cons nil cons 1516 def cons nil cons cons 1500 ref 212 ref 216 ref 1485 remove 1503 ref appTerm 1504 ref appTerm appTerm appTerm "Data.Word.*" const 1005 remove constTerm 1517 def 1505 remove appTerm 1506 remove appTerm appTerm absTerm 1518 def 1504 remove appTerm 1519 def betaConv 1501 remove 170 ref 1518 ref appTerm 1520 def absTerm 1521 def 1503 remove appTerm 1522 def betaConv nil 170 ref 1521 ref appTerm 1523 def axiom nil 43 ref 1523 remove nil cons cons 44 ref 1522 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1521 remove nil cons cons 1513 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1520 remove nil cons cons 44 ref 1519 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1518 remove nil cons cons 1514 remove cons nil cons cons 138 ref subst eqMp eqMp 1524 def subst appThm trans trans trans appThm 1473 ref refl 1475 ref refl nil 161 ref 249 ref nil cons 1525 def cons 8 ref 1476 ref nil cons cons nil cons cons nil cons cons 1105 remove subst 224 ref nil 161 ref 147 ref 1476 remove appTerm nil cons cons nil cons nil cons cons 161 ref 31 ref 1114 remove 249 ref appTerm appTerm 1486 ref 164 ref appTerm appTerm absTerm 1526 def 164 ref appTerm 1527 def betaConv nil 170 ref 1526 ref appTerm 1528 def axiom nil 43 ref 1528 remove nil cons cons 44 ref 1527 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1526 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst 1486 remove refl 231 ref nil 11 ref 847 remove cons nil cons nil cons cons 223 ref subst appThm appThm trans appThm nil 1500 remove 147 ref 216 ref 744 remove appTerm 1529 def appTerm nil cons cons 1516 remove cons nil cons cons 1524 remove subst 1517 remove 216 ref 250 remove appTerm appTerm 1530 def refl nil 155 ref 1529 ref nil cons cons nil cons nil cons cons 300 remove subst appThm trans trans trans 1531 def appThm appThm 1531 remove appThm appThm sym nil 43 ref 22 ref 751 ref appTerm 1532 def 370 ref appTerm 1533 def nil cons 1534 def cons 44 ref 212 ref 1515 remove 1530 remove 1529 remove appTerm 1535 def appTerm appTerm 1473 remove 1475 remove 1535 ref appTerm 1536 def appTerm 1535 ref appTerm appTerm nil cons 1537 def cons nil cons 1538 def cons nil cons cons 1539 def 61 ref subst 1539 remove 127 ref subst 22 ref "_31000" 3 ref var 1540 def 212 ref 1474 ref 216 ref 1176 ref 1540 remove varTerm 1541 def appTerm 249 ref appTerm 226 ref appTerm appTerm appTerm 1535 ref appTerm appTerm 1472 ref 1541 remove appTerm 1536 ref appTerm 1535 ref appTerm appTerm absTerm 1542 def 751 ref appTerm 1543 def appTerm refl 1544 def 1542 ref 370 ref appTerm betaConv appThm 89 ref 1543 remove betaConv appThm 1545 def 212 ref 1474 ref 216 ref 1176 ref 370 ref appTerm 249 ref appTerm 226 ref appTerm appTerm appTerm 1535 ref appTerm appTerm 1472 ref 370 ref appTerm 1536 ref appTerm 1535 ref appTerm appTerm refl appThm trans 1542 remove refl 1546 def 1533 remove assume appThm eqMp sym 273 ref 1474 ref refl 1547 def 224 ref nil 883 remove 232 remove cons 884 remove 1525 remove cons nil cons cons nil cons cons 1548 def 187 remove 983 ref subst subst appThm appThm 1535 ref refl 1549 def appThm nil 155 ref 1535 ref nil cons 1550 def cons nil cons nil cons cons 1551 def 155 ref 212 ref 1474 ref 230 remove appTerm 286 ref appTerm appTerm 286 ref appTerm absTerm 1552 def 286 remove appTerm 1553 def betaConv nil 6 ref 1552 ref appTerm 1554 def axiom nil 43 ref 1554 remove nil cons cons 44 ref 1553 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 ref 154 ref 1552 remove nil cons cons 291 remove cons nil cons cons 138 ref subst eqMp eqMp subst trans appThm nil "t2" 2 ref var 1555 def 1550 remove cons "t1" 2 remove var 1556 def 1536 ref nil cons 1557 def cons nil cons cons nil cons cons 1558 def 197 ref 983 remove subst 1559 def subst appThm 1551 remove 301 ref subst trans sym 79 ref eqMp eqMp eqMp nil 86 ref 1534 ref cons 87 ref 1537 ref cons nil cons 1560 def cons nil cons cons 101 ref subst deductAntisym eqMp nil 43 ref 1532 remove 66 ref appTerm 1561 def nil cons 1562 def cons 1538 remove cons nil cons cons 1563 def 61 ref subst 1563 remove 127 ref subst 1544 remove "_30998" 3 ref var 1564 def 212 ref 1474 ref 216 ref 1176 ref 1564 remove varTerm 1565 def appTerm 249 ref appTerm 226 ref appTerm appTerm appTerm 1535 ref appTerm appTerm 1472 ref 1565 remove appTerm 1536 ref appTerm 1535 ref appTerm appTerm absTerm 66 ref appTerm betaConv appThm 1545 remove 212 ref 1474 remove 216 ref 1176 ref 66 ref appTerm 249 remove appTerm 226 ref appTerm appTerm appTerm 1535 ref appTerm appTerm 1472 ref 66 remove appTerm 1536 remove appTerm 1535 remove appTerm appTerm refl appThm trans 1546 remove 1561 remove assume appThm eqMp sym 273 ref 1547 remove 224 ref 1548 remove 1191 remove subst appThm appThm 1549 remove appThm appThm 1558 remove 197 remove 445 remove subst 1566 def subst appThm nil 155 ref 1557 remove cons nil cons nil cons cons 301 remove subst trans sym 79 ref eqMp eqMp eqMp nil 86 ref 1562 remove cons 1567 def 1560 remove cons nil cons cons 101 ref subst deductAntisym eqMp 74 ref 722 ref 78 remove appTerm 77 remove 370 ref appTerm appTerm absTerm 1568 def 751 remove appTerm 1569 def betaConv nil 200 ref 1568 ref appTerm 1570 def axiom nil 43 ref 1570 remove nil cons cons 44 ref 1569 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1568 remove nil cons cons 881 remove cons nil cons cons 138 ref subst eqMp eqMp nil 1567 remove 87 ref 1534 remove cons 1329 ref 1537 remove cons nil cons cons cons nil cons cons 1343 ref subst proveHyp proveHyp proveHyp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 200 ref 1481 remove appTerm thm nil 110 ref 11 ref 170 ref 161 ref 45 ref 1469 ref appTerm 1571 def 212 ref "Data.Word.shiftRight" const 1087 remove constTerm 1572 def 214 remove appTerm 164 ref appTerm 1573 def appTerm 1574 def 1472 ref 364 remove 164 ref appTerm 1575 def appTerm 1576 def 229 ref appTerm 213 ref "Data.List.drop" const 374 remove constTerm 1577 def 164 ref appTerm 1578 def 25 ref appTerm 1579 def appTerm appTerm 1580 def appTerm 1581 def appTerm 1582 def absTerm 1583 def appTerm 1584 def absTerm 1585 def nil cons cons 1586 def nil cons nil cons cons 330 ref subst 11 ref nil 74 ref 1584 remove nil cons cons nil cons nil cons cons 80 ref subst nil 177 ref 1583 remove nil cons cons nil cons nil cons cons 525 ref subst 161 ref nil 74 ref 1582 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 1469 ref nil cons 1587 def cons 1588 def 44 ref 1581 remove nil cons 1589 def cons nil cons 1590 def cons nil cons cons 1591 def 61 ref subst 1591 ref 127 ref subst 140 ref 231 ref 345 ref 161 ref 212 ref 1572 ref 14 ref appTerm 164 ref appTerm appTerm 216 ref "Number.Natural.Bits.shiftRight" const 237 remove constTerm 1592 def 148 remove appTerm 164 ref appTerm appTerm appTerm absTerm 1593 def 164 ref appTerm 1594 def betaConv 8 remove 170 ref 1593 ref appTerm 1595 def absTerm 1596 def 14 remove appTerm 1597 def betaConv nil 6 remove 1596 ref appTerm 1598 def axiom nil 43 ref 1598 remove nil cons cons 44 ref 1597 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 153 remove 154 remove 1596 remove nil cons cons 156 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1595 remove nil cons cons 44 ref 1594 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1593 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst 224 ref 1592 ref refl 1599 def 346 remove appThm 1106 ref appThm appThm trans appThm appThm 231 ref 1576 remove refl 228 remove appThm nil 11 ref 1579 ref nil cons cons nil cons nil cons cons 223 remove subst appThm appThm appThm sym 140 remove nil 161 ref 1592 ref 147 ref 219 remove appTerm 1600 def appTerm 164 ref appTerm nil cons cons nil cons nil cons cons 269 ref subst nil 1109 ref 1107 ref 161 ref 1600 remove nil cons cons nil cons cons cons nil cons cons 158 ref 31 ref 238 ref 1592 ref 164 ref appTerm 165 ref appTerm appTerm 1111 ref appTerm 1601 def appTerm 1592 ref 239 remove 1116 remove appTerm appTerm 165 ref appTerm 1602 def appTerm 1603 def absTerm 1604 def 165 ref appTerm 1605 def betaConv 1108 ref 170 ref 1604 ref appTerm 1606 def absTerm 1607 def 1111 remove appTerm 1608 def betaConv 161 ref 170 ref 1607 ref appTerm 1609 def absTerm 1610 def 164 ref appTerm 1611 def betaConv 242 ref 161 ref 242 ref 1108 ref 242 ref 158 ref 1603 remove assume sym 31 ref 1602 remove appTerm 1601 remove appTerm 1612 def assume sym deductAntisym absThm appThm absThm appThm absThm appThm nil 170 ref 161 ref 170 ref 1108 remove 170 ref 158 ref 1612 remove absTerm appTerm absTerm appTerm absTerm appTerm axiom eqMp nil 43 ref 170 ref 1610 ref appTerm nil cons cons 44 ref 1611 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1610 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1609 remove nil cons cons 44 ref 1608 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1607 remove nil cons cons 1128 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1606 remove nil cons cons 44 ref 1605 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1604 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp 1613 def subst trans 1599 ref 238 remove refl 1614 def 349 remove appThm 1190 ref appThm nil 158 ref 1133 remove cons 1110 remove cons nil cons cons 1145 remove subst 452 remove refl 1192 remove appThm trans 1615 def trans appThm 1106 ref appThm trans appThm 231 remove nil "f" 215 remove var 216 remove nil cons cons 1616 def 732 remove 1616 remove 690 remove 217 ref 1579 remove appTerm nil cons cons 1493 ref 1575 remove nil cons cons nil cons cons cons cons cons nil cons cons 175 remove "B" 152 remove cons nil cons cons 186 remove cons 691 ref 1312 ref 359 remove 1 ref 3 ref 1 ref 668 ref 1 ref 668 remove 1260 remove cons opType nil cons cons opType nil cons cons opType constTerm 1494 ref appTerm 1264 ref 123 ref appTerm appTerm 1264 ref 692 ref appTerm appTerm 1617 def appTerm 1264 ref 433 ref 1494 ref appTerm 123 ref appTerm 692 ref appTerm appTerm 1618 def appTerm 1619 def absTerm 1620 def 692 ref appTerm 1621 def betaConv 122 ref 117 ref 1620 ref appTerm 1622 def absTerm 1623 def 123 ref appTerm 1624 def betaConv 1263 ref 117 ref 1623 ref appTerm 1625 def absTerm 1626 def 1264 remove appTerm 1627 def betaConv 1493 ref 1272 ref 1626 ref appTerm 1628 def absTerm 1629 def 1494 remove appTerm 1630 def betaConv 664 remove 1493 ref 1272 ref refl 1263 ref 117 ref refl 1631 def 122 ref 1631 remove 691 ref 1619 remove assume sym 1312 remove 1618 remove appTerm 1617 remove appTerm 1632 def assume sym deductAntisym absThm appThm absThm appThm absThm appThm absThm appThm nil 200 ref 1493 remove 1272 remove 1263 remove 117 ref 122 ref 117 ref 691 ref 1632 remove absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm axiom eqMp nil 43 ref 200 ref 1629 ref appTerm nil cons cons 44 ref 1630 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1629 remove nil cons cons 1498 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1628 remove nil cons cons 44 ref 1627 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 1274 remove 1275 remove 1626 remove nil cons cons 1276 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1625 remove nil cons cons 44 ref 1624 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 1623 remove nil cons cons 415 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1622 remove nil cons cons 44 ref 1621 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 1620 remove nil cons cons 699 ref cons nil cons cons 138 ref subst eqMp eqMp subst subst 224 remove 1153 remove 158 ref 31 ref 1176 remove 365 remove appTerm 226 remove appTerm 217 remove 1577 remove 165 ref appTerm 25 ref appTerm appTerm appTerm 1633 def appTerm 1592 remove 218 ref appTerm 1634 def 165 ref appTerm 1635 def appTerm 1636 def absTerm 1637 def 165 ref appTerm 1638 def betaConv 11 ref 170 ref 1637 ref appTerm 1639 def absTerm 1640 def 25 ref appTerm 1641 def betaConv 665 remove 11 ref 242 ref 158 ref 1636 remove assume sym 31 ref 1635 remove appTerm 1633 remove appTerm 1642 def assume sym deductAntisym absThm appThm absThm appThm nil 41 ref 11 ref 170 ref 158 ref 1642 remove absTerm appTerm absTerm appTerm axiom eqMp nil 43 ref 41 ref 1640 ref appTerm nil cons cons 44 ref 1641 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 1640 remove nil cons cons 113 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1639 remove nil cons cons 44 ref 1638 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1637 remove nil cons cons 182 ref cons nil cons cons 138 ref subst eqMp eqMp subst appThm trans appThm nil 161 ref 1634 remove 164 ref appTerm nil cons cons nil cons nil cons cons 269 remove subst nil 1109 remove 1107 remove 348 remove cons cons nil cons cons 1613 remove subst trans trans appThm sym 1599 remove 352 remove 158 remove 22 ref 257 remove 164 ref appTerm appTerm 308 remove appTerm absTerm 1643 def 165 remove appTerm 1644 def betaConv 161 ref 170 ref 1643 ref appTerm 1645 def absTerm 1646 def 164 ref appTerm 1647 def betaConv nil 170 ref 1646 ref appTerm 1648 def axiom nil 43 ref 1648 remove nil cons cons 44 ref 1647 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1646 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1645 remove nil cons cons 44 ref 1644 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1643 remove nil cons cons 182 remove cons nil cons cons 138 ref subst eqMp eqMp subst sym 161 ref 50 ref 306 ref 307 remove 218 ref appTerm 1649 def appTerm 1650 def 164 ref appTerm appTerm 388 ref 37 ref appTerm appTerm absTerm 1651 def 36 ref appTerm betaConv sym 455 ref nil 74 ref 1650 ref 36 ref appTerm 1652 def nil cons cons nil cons nil cons cons 80 ref subst 11 ref 1652 remove absTerm 1653 def 25 ref appTerm 1654 def betaConv nil 41 ref 1653 ref appTerm 1655 def axiom nil 43 ref 1655 remove nil cons cons 44 ref 1654 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 110 ref 1653 remove nil cons cons 113 ref cons nil cons cons 138 ref subst eqMp eqMp eqMp appThm nil 74 ref 1587 ref cons nil cons nil cons cons 80 ref subst 1469 ref assume eqMp 1656 def appThm 471 ref trans sym 79 ref eqMp eqMp 176 ref 177 ref 1651 ref nil cons cons 178 ref 36 ref nil cons 1657 def cons nil cons cons nil cons cons 492 remove subst proveHyp nil 43 ref 493 ref 1651 remove appTerm nil cons cons 44 ref 1650 remove 37 ref appTerm nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp nil 494 ref 159 remove cons 495 ref 1649 remove nil cons cons nil cons cons nil cons cons 494 ref 45 ref 493 remove 161 ref 500 ref 388 ref 501 ref appTerm appTerm 1658 def absTerm 1659 def appTerm 1660 def appTerm 1661 def 498 remove 501 ref appTerm 1662 def appTerm 1663 def absTerm 1664 def 501 ref appTerm 1665 def betaConv 495 ref 170 ref 1664 ref appTerm 1666 def absTerm 1667 def 497 ref appTerm 1668 def betaConv nil 170 ref 495 ref 170 ref 161 ref 170 ref 494 ref 45 ref 1658 ref appTerm 1662 ref appTerm absTerm 1669 def appTerm 1670 def absTerm 1671 def appTerm 1672 def absTerm 1673 def appTerm 1674 def axiom nil 43 ref 1674 ref nil cons 1675 def cons 1676 def 44 ref 170 ref 1667 ref appTerm nil cons 1677 def cons nil cons cons nil cons cons 1678 def 108 ref subst proveHyp 1678 ref 61 ref subst 1678 remove 127 ref subst nil 177 ref 1667 remove nil cons cons 1679 def nil cons nil cons cons 525 ref subst 495 ref nil 74 ref 1666 remove nil cons 1680 def cons nil cons nil cons cons 80 ref subst nil 177 ref 1664 remove nil cons cons 1681 def nil cons nil cons cons 525 ref subst 494 remove nil 74 ref 1663 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 1660 remove nil cons 1682 def cons 1683 def 44 ref 1662 ref nil cons 1684 def cons nil cons 1685 def cons nil cons cons 1686 def 61 ref subst 1686 remove 127 ref subst nil 1676 ref 1685 ref cons nil cons cons 1687 def 108 ref subst nil 1683 remove 44 ref 45 ref 1674 remove appTerm 1662 remove appTerm 1688 def nil cons 1689 def cons nil cons 1690 def cons nil cons cons 108 ref subst nil 177 ref 161 ref 45 ref 1659 ref 164 ref appTerm 1691 def appTerm 1688 ref appTerm 1692 def absTerm nil cons cons nil cons nil cons cons 525 ref subst 161 ref nil 74 ref 1692 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 1691 ref nil cons 1693 def cons 1690 ref cons nil cons cons 1694 def 61 ref subst 1694 remove 127 ref subst 1691 ref betaConv 1691 remove assume eqMp nil 43 ref 1658 remove nil cons 1695 def cons 1696 def 1690 remove cons nil cons cons 1697 def 108 ref subst proveHyp 1697 ref 61 ref subst 1697 remove 127 ref subst 1687 ref 61 ref subst 1687 remove 127 ref subst nil 1696 remove 1685 remove cons nil cons cons 108 ref subst 1669 ref 501 remove appTerm 1698 def betaConv 1671 ref 164 ref appTerm 1699 def betaConv 1673 ref 497 ref appTerm 1700 def betaConv nil 1676 remove 44 ref 1700 remove nil cons cons nil cons cons nil cons cons 108 ref subst 176 ref 177 ref 1673 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1672 remove nil cons cons 44 ref 1699 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1671 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1670 remove nil cons cons 44 ref 1698 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1669 remove nil cons cons 548 ref cons nil cons cons 138 ref subst eqMp eqMp eqMp eqMp nil 86 ref 1675 remove cons 1701 def 87 ref 1684 remove cons nil cons 1702 def cons nil cons cons 101 ref subst deductAntisym eqMp eqMp nil 86 ref 1695 remove cons 87 ref 1689 remove cons nil cons 1703 def cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp nil 86 ref 1693 remove cons 1703 ref cons nil cons cons 101 ref subst deductAntisym eqMp eqMp absThm eqMp nil 43 ref 170 ref 178 ref 45 ref 1659 ref 552 remove appTerm appTerm 1688 ref appTerm absTerm appTerm nil cons cons 44 ref 1661 remove 1688 remove appTerm nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1659 remove nil cons cons 1703 remove cons nil cons cons 566 remove subst eqMp eqMp eqMp eqMp nil 86 ref 1682 remove cons 1702 remove cons nil cons cons 101 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp nil 1701 remove 87 ref 1677 ref cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp nil 43 ref 1677 remove cons 44 ref 1668 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 1679 remove 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1680 remove cons 44 ref 1665 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 1681 remove 548 remove cons nil cons cons 138 ref subst eqMp eqMp subst eqMp eqMp 31 ref 453 remove appTerm 1704 def refl 1705 def 1614 remove 1704 remove 218 remove appTerm assume sym appThm 1190 remove appThm appThm sym 1705 remove 1615 remove appThm nil 178 remove 496 remove cons nil cons nil cons cons 192 remove subst trans sym 79 ref eqMp eqMp proveHyp appThm 1106 ref appThm eqMp eqMp nil 43 ref 31 ref 147 ref 1573 ref appTerm appTerm 147 remove 1580 ref appTerm appTerm nil cons cons 1590 remove cons nil cons cons 108 ref subst proveHyp nil 950 remove 1580 ref nil cons 1706 def cons 155 remove 1573 remove nil cons cons nil cons cons nil cons cons 1199 remove subst eqMp 1707 def eqMp nil 86 ref 1587 ref cons 1708 def 87 ref 1589 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp 1709 def eqMp absThm eqMp eqMp absThm eqMp 1710 def nil 41 ref 1585 ref appTerm 1711 def thm nil 110 ref 11 ref 170 ref 161 ref 45 ref 306 ref 37 ref appTerm 1712 def 36 ref appTerm 1713 def appTerm 1714 def 1574 ref 1472 ref 1712 ref 164 ref appTerm appTerm 229 ref appTerm 213 ref 1578 ref 428 ref appTerm appTerm 1715 def appTerm 1716 def appTerm 1717 def appTerm 1718 def absTerm 1719 def appTerm 1720 def absTerm 1721 def nil cons cons nil cons nil cons cons 330 ref subst 11 ref nil 74 ref 1720 remove nil cons cons nil cons nil cons cons 80 ref subst nil 177 ref 1719 remove nil cons cons nil cons nil cons cons 525 ref subst 161 ref nil 74 ref 1718 remove nil cons cons nil cons nil cons cons 80 ref subst nil 43 ref 1713 ref nil cons 1722 def cons 44 ref 1717 remove nil cons 1723 def cons nil cons 1724 def cons nil cons cons 1725 def 61 ref subst 1725 ref 127 ref subst nil 43 ref 724 ref 38 ref appTerm nil cons 1726 def cons 1727 def 1724 ref cons nil cons cons 1728 def 61 ref subst 1728 remove 127 ref subst 273 ref 1572 ref refl 1729 def 345 remove 589 remove subst appThm 1106 ref appThm appThm 1716 ref refl 1730 def appThm sym 273 remove 1729 remove 595 ref 382 remove appThm appThm 1106 ref appThm appThm 1730 ref appThm sym 89 ref "_31004" 10 ref var 1731 def 212 ref 1572 ref 213 ref 1731 remove varTerm appTerm appTerm 164 ref appTerm appTerm 1716 ref appTerm absTerm 1732 def 1471 remove appTerm betaConv appThm 455 ref 1571 ref refl 1732 ref 1470 ref appTerm betaConv appThm appThm 45 ref 724 ref 1469 ref appTerm 1733 def appTerm 1734 def refl 1732 ref 428 ref appTerm betaConv appThm appThm appThm nil "_485" 10 ref var 430 ref cons "_482" 10 remove var 1470 ref nil cons cons "_483" 3 ref var 1735 def 1587 ref cons nil cons cons cons nil cons cons nil "_484" 23 remove var 1732 remove nil cons cons nil cons nil cons cons 328 remove nil 122 ref "_482" 114 ref var varTerm nil cons cons "c" 3 remove var 1736 def 1735 remove varTerm nil cons cons 129 ref "_484" 115 ref var varTerm nil cons cons 691 ref "_485" 114 remove var varTerm nil cons cons nil cons cons cons cons nil cons cons 691 remove 22 ref 130 ref 433 remove 1736 ref varTerm 1737 def appTerm 123 ref appTerm 692 ref appTerm appTerm appTerm 50 remove 45 ref 1737 ref appTerm 476 remove appTerm appTerm 45 ref 724 ref 1737 ref appTerm appTerm 130 ref 692 ref appTerm appTerm appTerm appTerm absTerm 1738 def 692 remove appTerm 1739 def betaConv 122 remove 117 ref 1738 ref appTerm 1740 def absTerm 1741 def 123 remove appTerm 1742 def betaConv 1736 remove 117 remove 1741 ref appTerm 1743 def absTerm 1744 def 1737 ref appTerm 1745 def betaConv 129 remove 200 ref 1744 ref appTerm 1746 def absTerm 1747 def 130 ref appTerm 1748 def betaConv nil 0 remove 133 remove constTerm 1747 ref appTerm 1749 def axiom nil 43 ref 1749 remove nil cons cons 44 ref 1748 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp "A" 188 remove cons nil cons "P" 116 remove var 1747 remove nil cons cons "x" 115 remove var 130 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1746 remove nil cons cons 44 ref 1745 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1744 remove nil cons cons 205 ref 1737 remove nil cons cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1743 remove nil cons cons 44 ref 1742 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 ref 118 ref 1741 remove nil cons cons 415 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1740 remove nil cons cons 44 ref 1739 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 414 remove 118 remove 1738 remove nil cons cons 699 remove cons nil cons cons 138 ref subst eqMp eqMp subst subst subst subst eqMp sym nil 1588 ref 44 ref 212 ref 1572 ref 213 ref 1470 remove appTerm appTerm 164 ref appTerm appTerm 1716 ref appTerm 1750 def nil cons 1751 def cons nil cons cons nil cons cons 1752 def 61 ref subst 1752 remove 127 ref subst nil 1727 remove 797 remove cons nil cons cons 108 ref subst nil 74 ref 1726 ref cons nil cons nil cons cons 74 ref 22 ref 984 remove 370 ref appTerm appTerm 1299 ref appTerm absTerm 1753 def 76 ref appTerm 1754 def betaConv nil 200 ref 1753 ref appTerm 1755 def axiom nil 43 ref 1755 remove nil cons cons 44 ref 1754 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 ref 1753 remove nil cons cons 206 ref cons nil cons cons 138 ref subst eqMp eqMp subst nil 74 ref 331 ref cons nil cons nil cons cons 74 ref 22 ref 724 ref 1299 remove appTerm appTerm 76 ref appTerm absTerm 1756 def 76 remove appTerm 1757 def betaConv nil 200 remove 1756 ref appTerm 1758 def axiom nil 43 ref 1758 remove nil cons cons 44 ref 1757 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 204 remove 1756 remove nil cons cons 206 remove cons nil cons cons 138 ref subst eqMp eqMp subst nil 385 remove 495 ref 1657 ref cons 1759 def nil cons cons nil cons cons 161 ref 22 ref 834 ref appTerm 500 remove 388 ref 497 ref appTerm appTerm 1760 def appTerm 1761 def absTerm 1762 def 164 ref appTerm 1763 def betaConv 495 ref 170 ref 1762 ref appTerm 1764 def absTerm 1765 def 497 ref appTerm 1766 def betaConv 242 ref 495 ref 242 ref 161 ref 1761 remove assume sym 22 ref 1760 remove appTerm 834 remove appTerm 1767 def assume sym deductAntisym absThm appThm absThm appThm nil 170 ref 495 ref 170 ref 161 ref 1767 remove absTerm appTerm absTerm appTerm axiom eqMp nil 43 ref 170 ref 1765 ref appTerm nil cons cons 44 ref 1766 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1765 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1764 remove nil cons cons 44 ref 1763 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1762 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst trans trans 455 remove 1656 ref appThm nil 74 ref 1722 ref cons nil cons nil cons cons 80 ref subst 1713 remove assume eqMp 1768 def appThm 471 remove trans trans sym 79 ref eqMp eqMp nil 86 ref 1751 ref cons nil cons nil cons cons 806 remove subst proveHyp eqMp nil 1708 ref 87 ref 1751 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp nil 43 ref 1571 remove 1750 remove appTerm nil cons cons 44 ref 1734 remove 212 remove 1572 remove 213 remove 428 ref appTerm appTerm 164 ref appTerm appTerm 1769 def 1716 ref appTerm 1770 def appTerm nil cons cons nil cons cons nil cons cons 127 ref subst proveHyp nil 43 ref 1733 ref nil cons 1771 def cons 1772 def 44 ref 1770 ref nil cons 1773 def cons nil cons 1774 def cons nil cons cons 1775 def 61 ref subst 1775 remove 127 ref subst 161 ref 45 ref 306 ref 35 ref 428 ref appTerm 1776 def appTerm 1777 def 37 ref appTerm appTerm 1769 ref 1472 ref 1777 remove 164 ref appTerm appTerm 229 ref appTerm 1715 ref appTerm appTerm appTerm 1778 def absTerm 1779 def 164 ref appTerm 1780 def betaConv 1585 remove 428 remove appTerm 1781 def betaConv 1710 remove nil 43 ref 1711 remove nil cons cons 44 ref 1781 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 ref 1586 remove 111 remove 430 remove cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 170 ref 1779 ref appTerm nil cons cons 44 ref 1780 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1779 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1778 ref nil cons cons 1774 remove cons nil cons cons 108 ref subst proveHyp 11 ref 1714 remove 31 ref 1776 ref appTerm 37 ref appTerm 1782 def appTerm 1783 def absTerm 1784 def 25 ref appTerm 1785 def betaConv 161 ref 41 ref 11 ref 45 ref 388 ref 36 ref appTerm appTerm 31 ref 35 remove 375 ref 164 ref appTerm 25 ref appTerm appTerm appTerm 164 ref appTerm appTerm absTerm appTerm absTerm 1786 def 37 ref appTerm 1787 def betaConv 402 ref nil 170 ref 161 ref 422 ref 416 ref 45 ref 388 remove 704 ref appTerm appTerm 31 remove 701 remove 373 remove 1 remove 27 ref 417 remove cons opType constTerm 1788 def 164 ref appTerm 418 ref appTerm appTerm appTerm 164 ref appTerm appTerm absTerm appTerm absTerm appTerm axiom subst nil 43 ref 170 ref 1786 ref appTerm nil cons cons 44 ref 1787 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1786 remove nil cons cons 185 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 41 ref 1784 ref appTerm nil cons cons 44 ref 1785 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 109 remove 110 ref 1784 remove nil cons cons 113 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1783 remove nil cons cons 44 ref 45 ref 1778 remove appTerm 1770 ref appTerm 1789 def nil cons 1790 def cons nil cons 1791 def cons nil cons cons 108 ref subst proveHyp 689 ref 689 ref 1768 remove appThm 1782 ref refl appThm nil 74 ref 1782 ref nil cons 1792 def cons nil cons nil cons cons 932 ref subst trans appThm 1789 remove refl appThm sym nil 43 ref 1792 ref cons 1791 remove cons nil cons cons 1793 def 61 ref subst 1793 remove 127 ref subst 22 ref "_31010" 27 remove var 1794 def 45 ref 45 ref 306 remove 1794 remove varTerm appTerm 1795 def 37 ref appTerm appTerm 1769 remove 1472 ref 1795 remove 164 ref appTerm appTerm 229 ref appTerm 1715 remove appTerm appTerm appTerm appTerm 1770 ref appTerm absTerm 1796 def 1776 remove appTerm 1797 def appTerm refl 1796 ref 37 ref appTerm betaConv appThm 89 remove 1797 remove betaConv appThm 45 ref 45 ref 1712 remove 37 ref appTerm appTerm 1770 ref appTerm appTerm 1770 ref appTerm refl appThm trans 1796 remove refl 1782 remove assume appThm eqMp sym 689 ref 689 remove 393 remove appThm 1770 remove refl 1798 def appThm nil 74 ref 1773 ref cons nil cons nil cons cons 1799 def 932 remove subst trans appThm 1798 remove appThm 1799 remove 989 remove subst trans sym 79 ref eqMp eqMp eqMp nil 86 ref 1792 remove cons 87 ref 1790 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp eqMp eqMp nil 86 ref 1771 ref cons 1800 def 87 ref 1773 remove cons nil cons cons nil cons cons 101 ref subst deductAntisym eqMp eqMp eqMp eqMp eqMp eqMp nil 86 ref 1726 ref cons 87 ref 1723 ref cons nil cons 1801 def cons nil cons cons 101 ref subst deductAntisym eqMp nil 332 remove 1724 remove cons nil cons cons 1802 def 61 ref subst 1802 remove 127 ref subst 1574 ref refl 1803 def 1472 ref refl 1804 def 383 remove 384 remove sym 1805 def appThm 1106 remove appThm appThm 229 remove refl appThm 595 remove 1578 remove refl 375 remove refl 1805 remove appThm 25 remove refl appThm 402 remove 416 remove 407 remove 1788 remove 704 remove appTerm 418 ref appTerm appTerm 418 ref appTerm absTerm 1806 def 418 remove appTerm 1807 def betaConv nil 422 remove 1806 ref appTerm 1808 def axiom nil 43 ref 1808 remove nil cons cons 44 ref 1807 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 424 remove 425 remove 1806 remove nil cons cons 427 remove cons nil cons cons 138 ref subst eqMp eqMp subst trans appThm appThm appThm appThm sym 394 remove sym 79 ref eqMp 1591 remove 108 ref subst proveHyp 1709 remove eqMp eqMp eqMp nil 446 ref 1801 ref cons nil cons cons 101 ref subst deductAntisym eqMp 1323 ref 38 remove appTerm 1809 def betaConv 1326 ref nil 1327 ref 44 ref 1809 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 ref 1328 ref 205 ref 331 remove cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 446 remove 87 ref 1726 remove cons 1329 ref 1723 remove cons nil cons cons cons nil cons cons 1343 ref subst proveHyp proveHyp proveHyp eqMp nil 86 ref 1722 ref cons 1801 remove cons nil cons cons 101 ref subst deductAntisym eqMp 1810 def eqMp absThm eqMp eqMp absThm eqMp nil 41 ref 1721 remove appTerm thm nil 110 remove 11 ref 170 ref 161 ref 1574 remove 1472 remove 1469 ref appTerm 1580 ref appTerm 1716 ref appTerm appTerm 1811 def absTerm 1812 def appTerm 1813 def absTerm 1814 def nil cons cons nil cons nil cons cons 330 remove subst 11 remove nil 74 ref 1813 remove nil cons cons nil cons nil cons cons 80 ref subst nil 177 ref 1812 remove nil cons cons nil cons nil cons cons 525 remove subst 161 ref nil 74 remove 1811 remove nil cons 1815 def cons nil cons nil cons cons 80 remove subst 1323 remove 1469 ref appTerm 1816 def betaConv 1326 remove nil 1327 remove 44 ref 1816 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 203 remove 1328 remove 205 remove 1587 remove cons nil cons cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 722 remove 1469 ref appTerm 1733 remove appTerm nil cons 1817 def cons 44 ref 1815 ref cons nil cons 1818 def cons nil cons cons 1819 def 108 ref subst proveHyp 1819 ref 61 ref subst 1819 remove 127 ref subst nil 1772 ref 1818 ref cons nil cons cons 1820 def 61 ref subst 1820 remove 127 ref subst 1803 ref 1804 ref nil 1772 remove 44 ref 22 ref 1469 remove appTerm 370 remove appTerm nil cons cons nil cons cons nil cons cons 108 ref subst nil 1708 ref nil cons nil cons cons 807 remove subst eqMp 1821 def appThm 1580 remove refl 1822 def appThm 1730 ref appThm nil 1555 remove 1716 remove nil cons cons 1556 remove 1706 remove cons nil cons cons nil cons cons 1823 def 1559 remove subst trans appThm sym nil 1759 remove 386 remove cons nil cons cons 161 ref 22 ref 310 remove 497 ref appTerm 1824 def appTerm 724 remove 499 ref appTerm 1825 def appTerm 1826 def absTerm 1827 def 164 ref appTerm 1828 def betaConv 495 ref 170 ref 1827 ref appTerm 1829 def absTerm 1830 def 497 ref appTerm 1831 def betaConv 242 ref 495 ref 242 remove 161 ref 1826 remove assume sym 22 remove 1825 remove appTerm 1824 remove appTerm 1832 def assume sym deductAntisym absThm appThm absThm appThm nil 170 ref 495 ref 170 ref 161 ref 1832 remove absTerm appTerm absTerm appTerm axiom eqMp nil 43 ref 170 ref 1830 ref appTerm nil cons cons 44 ref 1831 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1830 remove nil cons cons 547 ref cons nil cons cons 138 ref subst eqMp eqMp nil 43 ref 1829 remove nil cons cons 44 ref 1828 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1827 remove nil cons cons 180 ref cons nil cons cons 138 ref subst eqMp eqMp subst 731 remove 1821 remove appThm 1298 remove trans trans sym 79 remove eqMp nil 43 ref 309 remove 37 remove appTerm 36 remove appTerm nil cons cons 44 ref 1722 remove cons nil cons cons nil cons cons 108 ref subst proveHyp nil 161 ref 1657 remove cons 1175 remove cons nil cons cons 161 remove 45 remove 937 remove appTerm 499 remove appTerm absTerm 1833 def 164 remove appTerm 1834 def betaConv 495 remove 170 ref 1833 ref appTerm 1835 def absTerm 1836 def 497 remove appTerm 1837 def betaConv nil 170 remove 1836 ref appTerm 1838 def axiom nil 43 ref 1838 remove nil cons cons 44 ref 1837 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 ref 177 ref 1836 remove nil cons cons 547 remove cons nil cons cons 138 ref subst eqMp eqMp nil 43 remove 1835 remove nil cons cons 44 remove 1834 remove nil cons cons nil cons cons nil cons cons 108 ref subst proveHyp 176 remove 177 remove 1833 remove nil cons cons 180 remove cons nil cons cons 138 remove subst eqMp eqMp subst eqMp 1725 remove 108 remove subst proveHyp 1810 remove eqMp eqMp eqMp nil 1800 remove 87 ref 1815 ref cons nil cons 1839 def cons nil cons cons 101 ref subst deductAntisym eqMp nil 1588 remove 1818 remove cons nil cons cons 1840 def 61 remove subst 1840 remove 127 remove subst 1803 remove 1804 remove 1656 remove appThm 1822 remove appThm 1730 remove appThm 1823 remove 1566 remove subst trans appThm sym 1707 remove eqMp eqMp nil 1708 ref 1839 ref cons nil cons cons 101 ref subst deductAntisym eqMp nil 1708 remove 87 remove 1771 remove cons 1329 remove 1815 remove cons nil cons cons cons nil cons cons 1343 remove subst proveHyp proveHyp eqMp nil 86 remove 1817 remove cons 1839 remove cons nil cons cons 101 remove subst deductAntisym eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 41 remove 1814 remove appTerm thm