path: "vendor/opentheory/data/theories/char-utf8-def/char-utf8-def.art"
6 version "Data.Char.UTF8.parseNatural" "Parser.orelse" const 0 def "->" typeOp 1 def "Parser.parser" typeOp 2 def "Data.Byte.byte" typeOp nil opType 3 def "Number.Natural.natural" typeOp nil opType 4 def nil cons 5 def cons 6 def opType 7 def 1 ref 7 ref 7 ref nil cons 8 def cons opType nil cons cons opType constTerm "Data.Char.UTF8.parseAscii" "Parser.token" const 9 def 1 ref 1 ref 3 ref "Data.Option.option" typeOp 10 def 5 ref opType 11 def nil cons 12 def cons opType 8 ref cons opType constTerm "b" 3 ref var 13 def "Data.Bool.cond" const 14 def 1 ref "bool" typeOp nil opType 15 def 1 ref 11 ref 1 ref 11 ref 12 ref cons opType nil cons cons opType nil cons cons opType constTerm 16 def "Data.Byte.bit" const 1 ref 3 ref 1 ref 4 ref 15 ref nil cons 17 def cons opType 18 def nil cons 19 def cons opType constTerm 20 def 13 ref varTerm 21 def appTerm 22 def "Number.Natural.bit1" const 1 ref 4 ref 5 ref cons opType 23 def constTerm 24 def 24 ref 24 ref "Number.Natural.zero" const 4 ref constTerm 25 def appTerm 26 def appTerm 27 def appTerm 28 def appTerm 29 def appTerm "Data.Option.none" const 30 def 11 ref constTerm 31 def appTerm "Data.Option.some" const 32 def 1 ref 4 ref 12 remove cons opType 33 def constTerm 34 def "Data.Byte.toNatural" const 1 ref 6 remove opType constTerm 35 def 21 ref appTerm appTerm appTerm absTerm appTerm 36 def defineConst 37 def pop 7 ref constTerm 38 def appTerm "Data.Char.UTF8.parseMultibyte" "Parser.sequence" const 1 ref 2 ref 3 ref 8 ref cons 39 def opType 40 def 8 ref cons opType constTerm 9 remove 1 ref 1 ref 3 ref 10 ref 8 ref opType 41 def nil cons 42 def cons opType 40 remove nil cons cons opType constTerm 13 ref 14 ref 1 ref 15 ref 1 ref 41 ref 1 ref 41 ref 42 ref cons opType nil cons cons opType nil cons cons opType constTerm 43 def 22 ref "Number.Natural.bit0" const 23 ref constTerm 44 def 27 ref appTerm 45 def appTerm 46 def appTerm 43 ref 22 ref 24 ref 44 ref 26 ref appTerm 47 def appTerm appTerm appTerm 43 ref 22 ref 44 ref 47 ref appTerm 48 def appTerm appTerm 43 remove 22 remove 27 remove appTerm appTerm 30 ref 41 remove constTerm 49 def appTerm 32 ref 1 ref 7 ref 42 remove cons opType constTerm 50 def "Data.Char.UTF8.parseMultibyte.parse4" "_32550" 3 ref var 51 def "Parser.filter" const 1 ref 7 ref 1 ref 18 ref 8 ref cons opType nil cons cons opType constTerm 52 def "Parser.foldN" const 1 ref 1 ref 3 ref 33 remove nil cons cons opType 53 def 1 ref 4 ref 1 ref 4 ref 8 remove cons opType nil cons cons opType nil cons cons opType constTerm "Data.Char.UTF8.parseMultibyte.addContinuationByte" "_32528" 3 ref var 54 def "_32529" 4 ref var 55 def 16 ref "Data.Char.UTF8.isContinuationByte" "_32523" 3 ref var 56 def "Data.Bool./\\" const 1 ref 15 ref 1 ref 15 ref 17 ref cons opType 57 def nil cons cons opType 58 def constTerm 59 def 20 remove 56 ref varTerm 60 def appTerm 61 def 28 ref appTerm appTerm "Data.Bool.~" const 57 remove constTerm 62 def 61 remove 45 ref appTerm appTerm appTerm 63 def absTerm 64 def defineConst 65 def pop 1 ref 3 ref 17 ref cons opType 66 def constTerm 67 def 54 ref varTerm 68 def appTerm appTerm 34 ref "Number.Natural.+" const 1 ref 4 ref 23 remove nil cons cons opType 69 def constTerm 70 def 35 ref "Data.Byte.and" const 1 ref 3 ref 1 ref 3 ref 3 ref nil cons 71 def cons 72 def opType nil cons cons opType 73 def constTerm 74 def 68 ref appTerm "Data.Byte.fromNatural" const 1 ref 4 ref 71 ref cons opType constTerm 75 def 24 ref 24 ref 24 remove 28 ref appTerm 76 def appTerm 77 def appTerm appTerm 78 def appTerm appTerm appTerm "Number.Natural.Bits.shiftLeft" const 69 ref constTerm 79 def 55 ref varTerm 80 def appTerm 45 ref appTerm appTerm appTerm appTerm 31 ref appTerm 81 def absTerm 82 def absTerm 83 def defineConst 84 def pop 53 remove constTerm 85 def appTerm 86 def 47 remove appTerm 87 def 35 ref 74 ref 51 ref varTerm 88 def appTerm 75 ref 28 ref appTerm 89 def appTerm appTerm appTerm appTerm "n" 4 ref var 90 def "Number.Natural.<=" const 1 ref 4 ref 19 remove cons opType 91 def constTerm 92 def 44 ref 44 ref 44 ref 44 ref 44 ref 44 ref 44 ref 44 ref 44 ref 44 ref 44 ref 44 ref 44 ref 44 ref 48 remove appTerm appTerm appTerm appTerm appTerm 93 def appTerm appTerm appTerm appTerm 94 def appTerm appTerm appTerm appTerm appTerm 95 def appTerm 90 ref varTerm 96 def appTerm absTerm 97 def appTerm 98 def absTerm 99 def defineConst 100 def pop 1 ref 39 remove opType 101 def constTerm 102 def 21 ref appTerm 103 def appTerm appTerm appTerm 50 ref "Data.Char.UTF8.parseMultibyte.parse3" "_32545" 3 ref var 104 def 52 ref 86 ref 26 remove appTerm 105 def 35 ref 74 ref 104 ref varTerm 106 def appTerm 75 ref 76 ref appTerm 107 def appTerm appTerm appTerm appTerm 90 ref 92 ref 94 ref appTerm 96 ref appTerm absTerm 108 def appTerm 109 def absTerm 110 def defineConst 111 def pop 101 ref constTerm 112 def 21 ref appTerm 113 def appTerm appTerm appTerm 50 remove "Data.Char.UTF8.parseMultibyte.parse2" "_32540" 3 ref var 114 def 52 ref 86 remove 25 remove appTerm 115 def 35 ref 74 ref 114 ref varTerm 116 def appTerm 75 ref 77 remove appTerm 117 def appTerm appTerm appTerm appTerm 90 ref 92 remove 93 ref appTerm 96 ref appTerm absTerm 118 def appTerm 119 def absTerm 120 def defineConst 121 def pop 101 remove constTerm 122 def 21 ref appTerm 123 def appTerm appTerm appTerm 49 remove appTerm absTerm appTerm appTerm 124 def defineConst 125 def pop 7 ref constTerm 126 def appTerm 127 def defineConst 128 def pop 129 def pop 128 remove nil "=" const 130 def 1 ref 7 ref 1 ref 7 ref 17 ref cons opType nil cons cons opType constTerm 131 def 129 remove 7 ref constTerm 132 def appTerm 127 remove appTerm thm nil "P" 18 ref var 133 def 90 ref 130 ref 1 ref "Data.List.list" typeOp 134 def 71 ref opType 135 def 1 ref 135 ref 17 ref cons opType 136 def nil cons cons opType constTerm 137 def "Data.Char.UTF8.encodeAscii" "_32483" 4 ref var 138 def "Data.List.::" const 1 ref 3 ref 1 ref 135 ref 135 ref nil cons 139 def cons opType nil cons 140 def cons opType constTerm 141 def 75 ref 138 ref varTerm 142 def appTerm appTerm "Data.List.[]" const 135 ref constTerm 143 def appTerm 144 def absTerm 145 def defineConst 146 def pop 1 ref 4 ref 139 ref cons opType 147 def constTerm 148 def 96 ref appTerm 149 def appTerm 141 ref 75 ref 96 ref appTerm appTerm 143 ref appTerm appTerm absTerm 150 def nil cons cons nil cons nil cons cons "A" 5 ref cons nil cons nil nil cons 151 def cons 130 ref 58 remove constTerm 152 def "Data.Bool.!" const 153 def 1 ref 1 ref "A" varType 154 def 17 ref cons opType 155 def 17 ref cons opType 156 def constTerm 157 def "P" 155 ref var varTerm 158 def appTerm appTerm refl "p" 155 ref var 159 def 130 ref 1 ref 155 remove 156 ref nil cons cons opType constTerm 159 remove varTerm appTerm "x" 154 remove var "Data.Bool.T" const 15 ref constTerm 160 def absTerm appTerm absTerm 161 def 158 ref appTerm betaConv appThm nil 130 ref 1 ref 156 ref 1 ref 156 remove 17 ref cons opType nil cons cons opType constTerm 157 remove appTerm 161 remove appTerm axiom 158 remove refl appThm eqMp sym 162 def subst 163 def subst 138 remove nil "t" 15 ref var 164 def 137 ref 148 remove 142 ref appTerm appTerm 144 remove appTerm nil cons cons nil cons nil cons cons 152 ref 164 ref varTerm 165 def appTerm 160 ref appTerm assume sym nil 160 remove axiom 166 def eqMp 165 remove assume 166 remove deductAntisym deductAntisym 167 def subst 146 remove 142 ref refl appThm 145 remove 142 remove appTerm betaConv trans eqMp absThm eqMp nil 153 ref 1 ref 18 ref 17 ref cons opType constTerm 168 def 150 remove appTerm thm nil "P" 1 ref 134 ref "Data.Char.char" typeOp nil opType 169 def nil cons 170 def opType 171 def 17 ref cons opType 172 def var "c" 171 ref var 173 def 137 ref "Data.Char.UTF8.encode" "_32508" 171 ref var 174 def "Data.List.concat" const 1 ref 134 ref 139 ref opType 175 def 139 ref cons opType constTerm 176 def "Data.List.map" const 177 def 1 ref 1 ref 169 ref 139 ref cons opType 178 def 1 ref 171 ref 175 remove nil cons 179 def cons opType nil cons cons opType constTerm "Data.Char.UTF8.encodeChar" "_32503" 169 ref var 180 def 90 ref 14 ref 1 ref 15 ref 1 ref 135 ref 140 remove cons opType nil cons cons opType constTerm 181 def "Number.Natural.<" const 91 remove constTerm 96 ref appTerm 182 def 93 ref appTerm appTerm 149 remove appTerm 181 ref 182 ref 94 remove appTerm appTerm "Data.Char.UTF8.encodeChar.encode2" "_32488" 4 ref var 183 def "n1" 4 ref var 184 def "b0" 3 ref var 185 def "b1" 3 ref var 186 def 141 ref 185 ref varTerm appTerm 187 def 141 ref 186 ref varTerm appTerm 188 def 143 ref appTerm appTerm absTerm 189 def "Data.Byte.or" const 73 remove constTerm 190 def 75 ref 93 remove appTerm appTerm 191 def 75 ref "Number.Natural.Bits.bound" const 69 ref constTerm 192 def 183 ref varTerm 193 def appTerm 45 ref appTerm appTerm appTerm appTerm absTerm 190 ref 75 ref 44 ref 44 ref 44 ref 44 ref 44 ref 45 ref appTerm appTerm appTerm appTerm appTerm appTerm appTerm 75 ref 184 ref varTerm 194 def appTerm appTerm 195 def appTerm absTerm "Number.Natural.Bits.shiftRight" const 69 remove constTerm 196 def 193 ref appTerm 45 ref appTerm appTerm 197 def absTerm 198 def defineConst 199 def pop 147 ref constTerm 200 def 96 ref appTerm 201 def appTerm 181 remove 182 remove 95 remove appTerm appTerm "Data.Char.UTF8.encodeChar.encode3" "_32493" 4 ref var 202 def 184 ref "n2" 4 ref var 203 def 185 ref 186 ref "b2" 3 ref var 204 def 187 ref 188 ref 141 ref 204 ref varTerm appTerm 205 def 143 ref appTerm appTerm appTerm absTerm 206 def 191 ref 75 ref 192 ref 202 ref varTerm 207 def appTerm 45 ref appTerm appTerm appTerm appTerm absTerm 191 ref 75 ref 192 ref 194 ref appTerm 45 ref appTerm appTerm appTerm 208 def appTerm absTerm 190 ref 75 ref 44 ref 44 ref 44 ref 44 ref 44 ref 28 remove appTerm appTerm appTerm appTerm appTerm appTerm appTerm 75 ref 203 ref varTerm 209 def appTerm appTerm 210 def appTerm absTerm 196 ref 194 remove appTerm 45 ref appTerm 211 def appTerm absTerm 196 ref 207 ref appTerm 45 ref appTerm appTerm 212 def absTerm 213 def defineConst 214 def pop 147 ref constTerm 215 def 96 ref appTerm 216 def appTerm "Data.Char.UTF8.encodeChar.encode4" "_32498" 4 ref var 217 def 184 ref 203 ref "n3" 4 ref var 218 def 185 ref 186 ref 204 ref "b3" 3 ref var 219 def 187 remove 188 remove 205 remove 141 ref 219 remove varTerm appTerm 143 ref appTerm appTerm appTerm appTerm absTerm 220 def 191 ref 75 ref 192 ref 217 ref varTerm 221 def appTerm 45 ref appTerm appTerm appTerm appTerm absTerm 208 ref appTerm absTerm 191 ref 75 ref 192 ref 209 ref appTerm 45 ref appTerm appTerm appTerm 222 def appTerm absTerm 190 remove 75 ref 44 ref 44 ref 44 ref 44 remove 76 remove appTerm appTerm appTerm appTerm appTerm appTerm 75 ref 218 ref varTerm appTerm appTerm 223 def appTerm absTerm 196 ref 209 remove appTerm 45 ref appTerm 224 def appTerm absTerm 211 ref appTerm absTerm 196 ref 221 ref appTerm 45 ref appTerm appTerm 225 def absTerm 226 def defineConst 227 def pop 147 remove constTerm 228 def 96 ref appTerm 229 def appTerm appTerm appTerm absTerm 230 def "Data.Char.dest" const 1 ref 169 ref 5 remove cons opType constTerm 231 def 180 ref varTerm 232 def appTerm appTerm 233 def absTerm 234 def defineConst 235 def pop 178 ref constTerm 236 def appTerm 237 def 174 ref varTerm 238 def appTerm appTerm 239 def absTerm 240 def defineConst 241 def pop 1 ref 171 ref 139 ref cons opType constTerm 242 def 173 remove varTerm 243 def appTerm appTerm 176 ref 237 remove 243 remove appTerm appTerm appTerm absTerm 244 def nil cons cons nil cons nil cons cons "A" 171 remove nil cons cons nil cons 151 ref cons 162 ref subst subst 174 remove nil 164 ref 137 ref 242 remove 238 ref appTerm appTerm 239 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 241 remove 238 ref refl appThm 240 remove 238 remove appTerm betaConv trans eqMp absThm eqMp nil 153 ref 1 ref 172 remove 17 ref cons opType constTerm 244 remove appTerm thm nil "P" 1 ref 134 remove "Data.Sum.+" typeOp 3 ref 170 ref cons 245 def opType 246 def nil cons 247 def opType 248 def 17 ref cons 249 def opType 250 def var "c" 248 ref var 251 def 137 ref "Data.Char.UTF8.reencode" "_32518" 248 ref var 252 def 176 ref 177 remove 1 ref 1 ref 246 ref 139 ref cons opType 253 def 1 ref 248 ref 179 remove cons opType nil cons cons opType constTerm "Data.Char.UTF8.reencodeChar" "_32513" 246 ref var 254 def "Data.Sum.case.left.right" const 1 ref 1 ref 3 ref 139 ref cons opType 1 ref 178 remove 253 ref nil cons cons opType nil cons cons opType constTerm 13 ref 141 remove 21 ref appTerm 143 remove appTerm absTerm appTerm "c" 169 ref var 255 def 236 ref 255 ref varTerm 256 def appTerm 257 def absTerm appTerm 258 def 254 ref varTerm 259 def appTerm 260 def absTerm 261 def defineConst 262 def pop 253 remove constTerm 263 def appTerm 264 def 252 ref varTerm 265 def appTerm appTerm 266 def absTerm 267 def defineConst 268 def pop 1 ref 248 ref 139 ref cons opType constTerm 269 def 251 remove varTerm 270 def appTerm appTerm 176 remove 264 remove 270 remove appTerm appTerm appTerm absTerm 271 def nil cons cons nil cons nil cons cons "A" 248 ref nil cons 272 def cons nil cons 151 ref cons 162 ref subst subst 252 remove nil 164 ref 137 ref 269 remove 265 ref appTerm appTerm 266 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 268 remove 265 ref refl appThm 267 remove 265 remove appTerm betaConv trans eqMp absThm eqMp nil 153 ref 1 ref 250 ref 17 ref cons opType constTerm 271 remove appTerm thm "Data.Char.UTF8.parse" 0 remove 1 ref 2 ref 3 remove 247 ref cons 273 def opType 274 def 1 ref 274 ref 274 ref nil cons 275 def cons opType nil cons cons opType constTerm "Parser.map" const 276 def 1 ref 2 ref 245 remove opType 277 def 1 ref 1 ref 169 ref 247 ref cons opType 278 def 275 ref cons opType nil cons cons opType constTerm "Data.Char.UTF8.parseChar" "Parser.mapPartial" const 1 ref 7 remove 1 ref 1 ref 4 ref 10 remove 170 ref opType 279 def nil cons 280 def cons opType 277 ref nil cons cons opType nil cons cons opType constTerm 132 remove appTerm 90 ref 14 remove 1 ref 15 remove 1 ref 279 ref 1 ref 279 ref 280 ref cons opType nil cons cons opType nil cons cons opType constTerm "Data.Char.invariant" const 18 remove constTerm 96 ref appTerm appTerm 32 remove 1 ref 169 ref 280 remove cons opType constTerm "Data.Char.mk" const 1 ref 4 remove 170 ref cons opType constTerm 96 ref appTerm appTerm appTerm 30 remove 279 remove constTerm appTerm absTerm appTerm 281 def defineConst 282 def pop 277 ref constTerm 283 def appTerm "Data.Sum.right" const 278 remove constTerm appTerm appTerm 276 remove 1 ref 2 remove 72 remove opType 284 def 1 ref 1 ref 273 remove opType 285 def 275 remove cons opType nil cons cons opType constTerm "Parser.any" const 284 remove constTerm appTerm "Data.Sum.left" const 285 remove constTerm appTerm appTerm 286 def defineConst 287 def pop 288 def pop 287 remove nil 130 ref 1 ref 274 ref 1 ref 274 ref 17 ref cons opType nil cons cons opType constTerm 288 remove 274 ref constTerm 289 def appTerm 286 remove appTerm thm nil "P" 136 ref var "b" 135 ref var 290 def 130 ref 1 ref 248 remove 250 remove nil cons cons opType constTerm 291 def "Data.Char.UTF8.decode" "_32555" 135 ref var 292 def "Data.Pair.fst" const 1 ref "Data.Pair.*" typeOp 249 remove opType 293 def 272 ref cons opType constTerm 294 def "Parser.Stream.toList" const 1 ref "Parser.Stream.stream" typeOp 295 def 247 ref opType 296 def 293 remove nil cons cons opType constTerm 297 def "Parser.parse" const 1 ref 274 remove 1 ref 295 remove 71 ref opType 298 def 296 remove nil cons cons opType nil cons cons opType constTerm 289 remove appTerm 299 def "Parser.Stream.fromList" const 1 ref 135 ref 298 remove nil cons cons opType constTerm 300 def 292 ref varTerm 301 def appTerm appTerm appTerm appTerm 302 def absTerm 303 def defineConst 304 def pop 1 ref 135 remove 272 remove cons opType constTerm 305 def 290 remove varTerm 306 def appTerm appTerm 294 remove 297 remove 299 remove 300 remove 306 remove appTerm appTerm appTerm appTerm appTerm absTerm 307 def nil cons cons nil cons nil cons cons "A" 139 remove cons nil cons 151 ref cons 162 ref subst subst 292 remove nil 164 ref 291 remove 305 remove 301 ref appTerm appTerm 302 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 304 remove 301 ref refl appThm 303 remove 301 remove appTerm betaConv trans eqMp absThm eqMp nil 153 ref 1 ref 136 remove 17 ref cons opType constTerm 307 remove appTerm thm 282 remove nil 130 ref 1 ref 277 ref 1 ref 277 remove 17 ref cons opType nil cons cons opType constTerm 283 remove appTerm 281 remove appTerm thm nil "P" 1 ref 246 ref 17 ref cons opType 308 def var "x" 246 remove var 309 def 137 ref 263 ref 309 remove varTerm 310 def appTerm appTerm 258 remove 310 remove appTerm appTerm absTerm 311 def nil cons cons nil cons nil cons cons "A" 247 remove cons nil cons 151 ref cons 162 ref subst subst 254 remove nil 164 ref 137 ref 263 remove 259 ref appTerm appTerm 260 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 262 remove 259 ref refl appThm 261 remove 259 remove appTerm betaConv trans eqMp absThm eqMp nil 153 ref 1 ref 308 remove 17 ref cons opType constTerm 311 remove appTerm thm 37 remove nil 131 ref 38 remove appTerm 36 remove appTerm thm nil "P" 66 ref var 312 def 13 ref 152 ref 67 ref 21 ref appTerm 313 def appTerm 59 remove 29 remove appTerm 62 remove 46 remove appTerm appTerm appTerm absTerm 314 def nil cons cons nil cons nil cons cons "A" 71 remove cons nil cons 151 ref cons 162 ref subst 315 def subst 56 remove nil 164 ref 152 remove 67 remove 60 ref appTerm appTerm 63 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 65 remove 60 ref refl appThm 64 remove 60 remove appTerm betaConv trans eqMp absThm eqMp nil 153 ref 1 ref 66 remove 17 ref cons opType constTerm 316 def 314 remove appTerm thm nil 312 ref 13 ref 168 ref 90 ref 130 remove 1 ref 11 ref 1 ref 11 remove 17 ref cons opType nil cons cons opType constTerm 317 def 85 ref 21 ref appTerm 96 ref appTerm appTerm 16 remove 313 remove appTerm 34 remove 70 remove 35 ref 74 remove 21 remove appTerm 318 def 78 remove appTerm appTerm appTerm 79 remove 96 ref appTerm 45 ref appTerm appTerm appTerm appTerm 31 remove appTerm appTerm absTerm appTerm absTerm 319 def nil cons cons nil cons nil cons cons 315 ref subst 54 remove nil 164 ref 168 ref 55 ref 317 remove 85 remove 68 ref appTerm 80 ref appTerm appTerm 81 remove appTerm 320 def absTerm 321 def appTerm nil cons cons nil cons nil cons cons 167 ref subst nil 133 ref 321 remove nil cons cons nil cons nil cons cons 163 ref subst 55 remove nil 164 ref 320 remove nil cons cons nil cons nil cons cons 167 ref subst 84 remove 68 ref refl appThm 83 remove 68 remove appTerm betaConv trans 80 ref refl appThm 82 remove 80 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 316 ref 319 remove appTerm thm nil 312 ref 13 ref 131 ref 123 remove appTerm 52 ref 115 remove 35 ref 318 ref 117 remove appTerm appTerm appTerm appTerm 118 remove appTerm appTerm absTerm 322 def nil cons cons nil cons nil cons cons 315 ref subst 114 remove nil 164 ref 131 ref 122 remove 116 ref appTerm appTerm 119 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 121 remove 116 ref refl appThm 120 remove 116 remove appTerm betaConv trans eqMp absThm eqMp nil 316 ref 322 remove appTerm thm nil 312 ref 13 ref 131 ref 113 remove appTerm 52 ref 105 remove 35 ref 318 ref 107 remove appTerm appTerm appTerm appTerm 108 remove appTerm appTerm absTerm 323 def nil cons cons nil cons nil cons cons 315 ref subst 104 remove nil 164 ref 131 ref 112 remove 106 ref appTerm appTerm 109 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 111 remove 106 ref refl appThm 110 remove 106 remove appTerm betaConv trans eqMp absThm eqMp nil 316 ref 323 remove appTerm thm nil 312 remove 13 remove 131 ref 103 remove appTerm 52 remove 87 remove 35 remove 318 remove 89 remove appTerm appTerm appTerm appTerm 97 remove appTerm appTerm absTerm 324 def nil cons cons nil cons nil cons cons 315 remove subst 51 remove nil 164 ref 131 ref 102 remove 88 ref appTerm appTerm 98 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 100 remove 88 ref refl appThm 99 remove 88 remove appTerm betaConv trans eqMp absThm eqMp nil 316 remove 324 remove appTerm thm 125 remove nil 131 remove 126 remove appTerm 124 remove appTerm thm nil 133 ref 90 ref 137 ref 201 remove appTerm 184 ref 185 ref 189 remove 191 remove 75 remove 192 remove 96 ref appTerm 45 ref appTerm appTerm appTerm 325 def appTerm absTerm 195 remove appTerm absTerm 196 remove 96 remove appTerm 45 remove appTerm 326 def appTerm appTerm absTerm 327 def nil cons cons nil cons nil cons cons 163 ref subst 183 remove nil 164 ref 137 ref 200 remove 193 ref appTerm appTerm 197 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 199 remove 193 ref refl appThm 198 remove 193 remove appTerm betaConv trans eqMp absThm eqMp nil 168 ref 327 remove appTerm thm nil "P" 1 ref 169 remove 17 ref cons opType 328 def var 255 remove 137 ref 257 remove appTerm 230 remove 231 remove 256 remove appTerm appTerm appTerm absTerm 329 def nil cons cons nil cons nil cons cons "A" 170 remove cons nil cons 151 remove cons 162 remove subst subst 180 remove nil 164 ref 137 ref 236 remove 232 ref appTerm appTerm 233 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 235 remove 232 ref refl appThm 234 remove 232 remove appTerm betaConv trans eqMp absThm eqMp nil 153 remove 1 remove 328 remove 17 remove cons opType constTerm 329 remove appTerm thm nil 133 ref 90 ref 137 ref 216 remove appTerm 184 ref 203 ref 185 ref 186 ref 206 remove 325 ref appTerm absTerm 208 ref appTerm absTerm 210 remove appTerm absTerm 211 ref appTerm absTerm 326 ref appTerm appTerm absTerm 330 def nil cons cons nil cons nil cons cons 163 ref subst 202 remove nil 164 ref 137 ref 215 remove 207 ref appTerm appTerm 212 remove appTerm nil cons cons nil cons nil cons cons 167 ref subst 214 remove 207 ref refl appThm 213 remove 207 remove appTerm betaConv trans eqMp absThm eqMp nil 168 ref 330 remove appTerm thm nil 133 remove 90 remove 137 ref 229 remove appTerm 184 remove 203 remove 218 remove 185 remove 186 remove 204 remove 220 remove 325 remove appTerm absTerm 208 remove appTerm absTerm 222 remove appTerm absTerm 223 remove appTerm absTerm 224 remove appTerm absTerm 211 remove appTerm absTerm 326 remove appTerm appTerm absTerm 331 def nil cons cons nil cons nil cons cons 163 remove subst 217 remove nil 164 remove 137 remove 228 remove 221 ref appTerm appTerm 225 remove appTerm nil cons cons nil cons nil cons cons 167 remove subst 227 remove 221 ref refl appThm 226 remove 221 remove appTerm betaConv trans eqMp absThm eqMp nil 168 remove 331 remove appTerm thm