path: "vendor/opentheory/data/theories/natural-add-sub-def/natural-add-sub-def.art"
6 version nil "P" "->" typeOp 0 def "Number.Natural.natural" typeOp nil opType 1 def "bool" typeOp nil opType 2 def nil cons 3 def cons opType 4 def var 5 def "m" 1 ref var 6 def "Data.Bool.!" const 7 def 0 ref 4 ref 3 ref cons opType 8 def constTerm 9 def "n" 1 ref var 10 def "=" const 11 def 0 ref 1 ref 4 ref nil cons 12 def cons opType constTerm 13 def "Number.Natural.-" "-" 0 ref 1 ref 0 ref 1 ref 1 ref nil cons 14 def cons opType 15 def nil cons 16 def cons opType 17 def var 18 def nil cons cons nil cons 18 ref "Data.Bool./\\" const 0 ref 2 ref 0 ref 2 ref 3 ref cons opType 19 def nil cons cons opType 20 def constTerm 21 def 9 ref 6 ref 13 ref 18 ref varTerm 22 def 6 ref varTerm 23 def appTerm 24 def "Number.Natural.zero" const 1 ref constTerm 25 def appTerm appTerm 23 ref appTerm absTerm appTerm appTerm 9 ref 6 ref 9 ref 10 ref 13 ref 24 ref "Number.Natural.suc" const 15 ref constTerm 26 def 10 ref varTerm 27 def appTerm 28 def appTerm appTerm "Number.Natural.pre" const 15 ref constTerm 29 def 24 remove 27 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 30 def refl 31 def 11 ref 0 ref 17 ref 0 ref 17 ref 3 ref cons opType 32 def nil cons cons opType constTerm 33 def 22 ref appTerm 34 def "select" const 35 def 0 ref 32 ref 17 ref nil cons 36 def cons opType constTerm 37 def 30 ref appTerm appTerm assume sym appThm 30 ref 22 ref appTerm betaConv 38 def trans "A" 36 ref cons nil cons 39 def nil nil cons 40 def cons 41 def nil 11 ref 0 ref 0 ref 0 ref "A" varType 42 def 3 ref cons opType 43 def 3 ref cons opType 44 def 0 ref 44 ref 3 ref cons opType nil cons cons opType constTerm 45 def "Data.Bool.?" const 46 def 44 ref constTerm 47 def appTerm 48 def "p" 43 ref var 49 def 49 ref varTerm 50 def 35 remove 0 ref 43 ref 42 ref nil cons 51 def cons opType constTerm 50 ref appTerm appTerm absTerm appTerm axiom subst 31 remove appThm "p" 32 ref var 52 def 52 remove varTerm 53 def 37 remove 53 remove appTerm appTerm absTerm 30 ref appTerm betaConv trans 46 ref 0 ref 32 ref 3 ref cons opType 54 def constTerm 55 def refl "fn" 17 ref var 56 def 21 ref 11 ref 0 ref 15 ref 0 ref 15 ref 3 ref cons opType nil cons cons opType constTerm 57 def 56 remove varTerm 58 def 25 ref appTerm appTerm 6 ref 23 ref absTerm 59 def appTerm appTerm refl 9 ref refl 60 def 10 ref 57 ref 58 ref 28 ref appTerm appTerm refl "_2229" 15 ref var 61 def 10 ref 6 ref 29 ref 61 remove varTerm 23 ref appTerm appTerm absTerm absTerm absTerm 62 def 58 remove 27 ref appTerm 63 def appTerm betaConv 27 ref refl 64 def appThm "n'" 1 ref var 6 ref 29 ref 63 remove 23 ref appTerm appTerm absTerm absTerm 27 ref appTerm betaConv trans appThm absThm appThm appThm absThm appThm nil "f" 0 ref 15 ref 36 remove cons opType var 62 remove nil cons cons "e" 15 remove var 59 ref nil cons cons nil cons cons nil cons cons "A" 16 remove cons nil cons 40 ref cons "f" 0 ref 42 ref 0 ref 1 ref 51 ref cons opType 65 def nil cons 66 def cons opType 67 def var 68 def "Data.Bool.?!" const 69 def 0 ref 0 ref 65 ref 3 ref cons opType 70 def 3 ref cons opType 71 def constTerm "fn" 65 remove var 72 def 21 ref 11 ref 0 ref 42 ref 43 ref nil cons cons opType constTerm 73 def 72 remove varTerm 74 def 25 ref appTerm appTerm "e" 42 ref var 75 def varTerm 76 def appTerm appTerm 9 ref 10 ref 73 ref 74 ref 28 ref appTerm appTerm 68 remove varTerm 77 def 74 remove 27 ref appTerm appTerm 27 ref appTerm appTerm absTerm appTerm appTerm absTerm 78 def appTerm 79 def absTerm 80 def 77 ref appTerm 81 def betaConv 75 remove 7 ref 0 ref 0 ref 67 ref 3 ref cons opType 82 def 3 ref cons opType constTerm 80 ref appTerm 83 def absTerm 84 def 76 ref appTerm 85 def betaConv nil 7 ref 44 ref constTerm 86 def 84 ref appTerm 87 def axiom nil "p" 2 ref var 88 def 87 remove nil cons cons "q" 2 ref var 89 def 85 remove nil cons cons nil cons cons nil cons cons 11 ref 20 ref constTerm 90 def "Data.Bool.==>" const 20 ref constTerm 91 def 88 ref varTerm 92 def appTerm 89 ref varTerm 93 def appTerm 94 def appTerm refl 88 ref 89 ref 90 ref 21 ref 92 ref appTerm 95 def 93 ref appTerm 96 def appTerm 97 def 92 ref appTerm absTerm 98 def absTerm 99 def 92 ref appTerm betaConv 93 ref refl 100 def appThm 98 remove 93 ref appTerm betaConv trans appThm nil 11 ref 0 ref 20 ref 0 ref 20 ref 3 ref cons opType 101 def nil cons cons opType constTerm 102 def 91 ref appTerm 99 remove appTerm axiom 92 ref refl 103 def appThm 100 ref appThm eqMp 104 def sym 105 def 97 remove refl 89 ref 11 ref 0 ref 101 ref 0 ref 101 remove 3 ref cons opType nil cons cons opType constTerm 106 def "f" 20 remove var 107 def 107 ref varTerm 108 def 92 ref appTerm 93 ref appTerm absTerm 109 def appTerm 107 ref 108 ref "Data.Bool.T" const 2 ref constTerm 110 def appTerm 110 ref appTerm absTerm 111 def appTerm absTerm 112 def 93 ref appTerm betaConv appThm 11 ref 0 ref 19 ref 0 ref 19 ref 3 ref cons opType 113 def nil cons cons opType constTerm 114 def 95 remove appTerm refl 88 ref 112 remove absTerm 115 def 92 ref appTerm betaConv appThm nil 102 remove 21 ref appTerm 115 ref appTerm axiom 116 def 103 remove appThm eqMp 100 ref appThm eqMp 117 def sym 107 ref 108 ref refl nil "t" 2 ref var 118 def 92 ref nil cons 119 def cons nil cons nil cons cons 90 ref 118 ref varTerm 120 def appTerm 110 ref appTerm assume sym nil 110 ref axiom 121 def eqMp 120 remove assume 121 ref deductAntisym deductAntisym 122 def subst 92 ref assume 123 def eqMp appThm nil 118 ref 93 ref nil cons 124 def cons nil cons nil cons cons 122 ref subst 93 ref assume eqMp appThm absThm eqMp 125 def nil "P" 2 ref var 126 def 119 remove cons "Q" 2 ref var 127 def 124 remove cons nil cons cons nil cons cons 90 ref refl 128 def 107 ref 108 remove 126 ref varTerm 129 def appTerm 130 def 127 ref varTerm 131 def appTerm absTerm 132 def 88 ref 89 ref 92 ref absTerm absTerm 133 def appTerm betaConv 133 ref 129 ref appTerm betaConv 131 ref refl 134 def appThm 89 ref 129 ref absTerm 131 ref appTerm betaConv trans trans appThm 111 ref 133 ref appTerm betaConv 133 ref 110 ref appTerm betaConv 110 ref refl 135 def appThm 89 ref 110 ref absTerm 110 ref appTerm betaConv trans trans appThm 90 ref 21 ref 129 ref appTerm 136 def 131 ref appTerm 137 def appTerm refl 89 ref 106 remove 107 remove 130 remove 93 ref appTerm absTerm appTerm 111 ref appTerm absTerm 131 ref appTerm betaConv appThm 114 remove 136 remove appTerm refl 115 remove 129 ref appTerm betaConv appThm 116 remove 129 ref refl appThm eqMp 134 ref appThm eqMp 137 remove assume eqMp 138 def 133 remove refl appThm eqMp sym 121 ref eqMp 139 def subst 140 def deductAntisym eqMp 104 remove 94 ref assume eqMp sym 123 ref eqMp 128 ref 109 remove 88 ref 89 ref 93 ref absTerm 141 def absTerm 142 def appTerm betaConv 142 ref 92 ref appTerm betaConv 100 remove appThm 141 ref 93 ref appTerm betaConv trans trans appThm 111 remove 142 ref appTerm betaConv 142 ref 110 ref appTerm betaConv 135 remove appThm 141 ref 110 ref appTerm betaConv trans trans 143 def appThm 117 remove 96 remove assume eqMp 142 ref refl 144 def appThm eqMp sym 121 ref eqMp 145 def proveHyp deductAntisym 146 def subst proveHyp "A" 51 remove cons nil cons 147 def "P" 43 ref var 148 def 84 remove nil cons cons "x" 42 ref var 149 def 76 remove nil cons cons nil cons cons nil cons cons nil 88 ref 86 ref 148 ref varTerm 150 def appTerm 151 def nil cons 152 def cons 89 ref 150 ref 149 ref varTerm 153 def appTerm 154 def nil cons 155 def cons nil cons cons nil cons cons 156 def 105 ref subst 156 remove 145 remove 125 remove deductAntisym 157 def subst 90 ref 154 ref appTerm refl 149 ref 110 remove absTerm 158 def 153 ref appTerm betaConv appThm 49 ref 11 remove 0 ref 43 remove 44 ref nil cons cons opType constTerm 50 ref appTerm 158 remove appTerm absTerm 159 def 150 ref appTerm betaConv 160 def nil 45 ref 86 ref appTerm 159 remove appTerm axiom 150 ref refl 161 def appThm 162 def 151 ref assume eqMp eqMp 153 ref refl 163 def appThm eqMp sym 121 ref eqMp eqMp nil 126 ref 152 remove cons 127 ref 155 ref cons nil cons cons nil cons cons 139 ref subst deductAntisym eqMp 164 def subst eqMp eqMp nil 88 ref 83 remove nil cons cons 89 ref 81 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp "A" 67 ref nil cons cons nil cons "P" 82 remove var 80 remove nil cons cons "x" 67 remove var 77 remove nil cons cons nil cons cons nil cons cons 164 ref subst eqMp eqMp nil 88 ref 79 remove nil cons cons 89 ref 46 remove 71 remove constTerm 78 ref appTerm nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp "A" 66 remove cons nil cons "P" 70 remove var 78 remove nil cons cons nil cons nil cons cons nil 88 ref 69 remove 44 remove constTerm 165 def 150 ref appTerm 166 def nil cons 167 def cons 168 def 89 ref 47 ref 150 ref appTerm 169 def nil cons 170 def cons nil cons cons nil cons cons 171 def 105 ref subst 171 remove 157 ref subst nil 168 remove 89 ref 21 ref 169 ref appTerm 86 ref 149 ref 86 ref "y" 42 remove var 172 def 91 ref 21 ref 154 ref appTerm 150 ref 172 ref varTerm 173 def appTerm appTerm appTerm 73 remove 153 ref appTerm 174 def 173 ref appTerm 175 def appTerm absTerm appTerm absTerm appTerm 176 def appTerm 177 def nil cons cons nil cons cons nil cons cons 178 def 146 ref subst 90 ref 166 ref appTerm 179 def refl 49 ref 21 ref 47 remove 50 ref appTerm appTerm 86 ref 149 ref 86 ref 172 remove 91 ref 21 ref 50 ref 153 ref appTerm 180 def appTerm 50 remove 173 remove appTerm appTerm appTerm 175 remove appTerm absTerm appTerm absTerm appTerm appTerm absTerm 181 def 150 ref appTerm betaConv appThm nil 45 remove 165 remove appTerm 181 remove appTerm axiom 161 ref appThm eqMp nil 88 ref 179 remove 177 ref appTerm nil cons cons 89 ref 91 ref 166 remove appTerm 177 remove appTerm nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 178 remove nil 88 ref 90 ref 92 remove appTerm 93 ref appTerm 182 def nil cons 183 def cons 89 ref 94 remove nil cons 184 def cons nil cons cons nil cons cons 185 def 105 ref subst 185 remove 157 ref subst 105 ref 157 ref 182 remove assume 123 remove eqMp eqMp 140 remove deductAntisym eqMp eqMp nil 126 ref 183 remove cons 127 ref 184 remove cons nil cons cons nil cons cons 139 ref subst deductAntisym eqMp 186 def subst eqMp eqMp nil 126 ref 170 ref cons 187 def 127 ref 176 remove nil cons cons nil cons cons nil cons cons 139 ref subst proveHyp eqMp nil 126 ref 167 remove cons 127 ref 170 ref cons nil cons cons nil cons cons 139 ref subst deductAntisym eqMp subst eqMp subst subst eqMp nil 88 ref 55 ref "_2228" 17 ref var 188 def 21 ref 57 ref 188 ref varTerm 189 def 25 ref appTerm 190 def appTerm 59 ref appTerm 191 def appTerm 9 ref 10 ref 57 remove 189 ref 28 ref appTerm 192 def appTerm 6 ref 29 ref 189 ref 27 ref appTerm 23 ref appTerm appTerm 193 def absTerm 194 def appTerm absTerm 195 def appTerm 196 def appTerm 197 def absTerm 198 def appTerm 199 def nil cons cons 89 ref 55 ref 188 ref 21 ref 9 ref 6 ref 13 ref 190 remove 23 ref appTerm appTerm 200 def 23 ref appTerm 201 def absTerm 202 def appTerm 203 def appTerm 9 ref 6 ref 9 ref 10 ref 13 ref 192 remove 23 ref appTerm appTerm 204 def 193 remove appTerm 205 def absTerm 206 def appTerm 207 def absTerm 208 def appTerm 209 def appTerm 210 def absTerm 211 def appTerm 212 def nil cons 213 def cons nil cons 214 def cons nil cons cons 146 ref subst nil "P" 32 remove var 215 def 188 ref 91 ref 198 ref 189 ref appTerm 216 def appTerm 212 ref appTerm 217 def absTerm nil cons cons nil cons nil cons cons 41 remove 90 ref 151 remove appTerm refl 160 remove appThm 162 remove eqMp sym 218 def subst 219 def subst 188 ref nil 118 ref 217 remove nil cons cons nil cons nil cons cons 122 ref subst nil 88 ref 216 ref nil cons 220 def cons 214 ref cons nil cons cons 221 def 105 ref subst 221 remove 157 ref subst 216 ref betaConv 216 remove assume eqMp nil 88 ref 197 remove nil cons 222 def cons 214 remove cons nil cons cons 223 def 146 ref subst proveHyp 223 ref 105 ref subst 223 remove 157 ref subst 211 ref 189 ref appTerm 224 def betaConv 225 def sym nil 126 ref 191 ref nil cons cons 127 ref 196 remove nil cons 226 def cons nil cons cons nil cons cons 227 def 139 ref subst nil 5 ref 202 remove nil cons cons nil cons nil cons cons "A" 14 remove cons nil cons 228 def 40 ref cons 229 def 218 ref subst 230 def subst 6 ref nil 118 ref 201 remove nil cons cons nil cons nil cons cons 122 ref subst 200 remove refl 59 remove 23 ref appTerm betaConv appThm 191 remove assume 23 ref refl 231 def appThm eqMp eqMp absThm eqMp proveHyp nil 88 ref 203 remove nil cons cons 89 ref 209 remove nil cons cons nil cons cons nil cons cons 157 ref subst proveHyp 227 remove 128 remove 132 remove 142 ref appTerm betaConv 142 remove 129 remove appTerm betaConv 134 remove appThm 141 remove 131 ref appTerm betaConv trans trans appThm 143 remove appThm 138 remove 144 remove appThm eqMp sym 121 ref eqMp 232 def subst nil 5 ref 208 remove nil cons cons nil cons nil cons cons 230 ref subst 6 ref nil 118 ref 207 remove nil cons cons nil cons nil cons cons 122 ref subst nil 5 ref 206 remove nil cons cons nil cons nil cons cons 230 ref subst 10 ref nil 118 ref 205 remove nil cons cons nil cons nil cons cons 122 ref subst 204 remove refl 194 remove 23 ref appTerm betaConv appThm 195 ref 27 ref appTerm 233 def betaConv nil 88 ref 226 remove cons 89 ref 233 remove nil cons cons nil cons cons nil cons cons 146 ref subst 228 ref 5 ref 195 remove nil cons cons "x" 1 ref var 234 def 27 ref nil cons cons nil cons 235 def cons nil cons cons 164 ref subst eqMp eqMp 231 ref appThm eqMp eqMp absThm eqMp eqMp absThm eqMp proveHyp eqMp eqMp 39 ref 215 ref 211 ref nil cons cons 236 def "x" 17 ref var 237 def 189 ref nil cons cons nil cons cons nil cons cons 90 remove 169 ref appTerm 238 def refl 49 remove 7 ref 113 remove constTerm 239 def 89 ref 91 ref 86 ref 149 ref 91 ref 180 remove appTerm 93 ref appTerm absTerm appTerm appTerm 93 ref appTerm absTerm appTerm absTerm 240 def 150 remove appTerm betaConv appThm nil 48 remove 240 remove appTerm axiom 161 remove appThm eqMp 241 def sym nil "P" 19 remove var 242 def 127 ref 91 ref 86 ref 149 ref 91 ref 154 remove appTerm 243 def 131 ref appTerm absTerm 244 def appTerm 245 def appTerm 131 ref appTerm 246 def absTerm nil cons cons nil cons nil cons cons "A" 3 ref cons nil cons 247 def 40 remove cons 218 remove subst subst 127 ref nil 118 ref 246 remove nil cons cons nil cons nil cons cons 122 ref subst nil 88 ref 245 remove nil cons 248 def cons 249 def 89 ref 131 ref nil cons 250 def cons nil cons 251 def cons nil cons cons 252 def 105 ref subst 252 ref 157 ref subst nil 88 ref 155 remove cons 251 ref cons nil cons cons 146 ref subst 244 ref 153 ref appTerm 253 def betaConv nil 249 ref 89 ref 253 remove nil cons cons nil cons cons nil cons cons 146 ref subst 147 remove 148 remove 244 remove nil cons cons 149 ref 153 ref nil cons cons nil cons cons nil cons cons 164 ref subst eqMp eqMp eqMp eqMp nil 126 ref 248 remove cons 254 def 127 ref 250 ref cons nil cons 255 def cons nil cons cons 139 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 256 def subst proveHyp eqMp nil 126 ref 222 remove cons 127 ref 213 ref cons nil cons 257 def cons nil cons cons 139 ref subst deductAntisym eqMp eqMp eqMp nil 126 ref 220 remove cons 257 ref cons nil cons cons 139 ref subst deductAntisym eqMp eqMp absThm eqMp nil 88 ref 7 ref 54 remove constTerm 258 def 237 ref 91 ref 198 ref 237 ref varTerm 259 def appTerm appTerm 212 ref appTerm absTerm appTerm nil cons cons 89 ref 91 ref 199 remove appTerm 212 ref appTerm nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 39 ref 215 ref 198 remove nil cons cons 257 remove cons nil cons cons nil 249 remove 89 ref 91 ref 169 remove appTerm 260 def 131 ref appTerm nil cons 261 def cons nil cons cons nil cons cons 262 def 105 ref subst 262 remove 157 ref subst nil 88 ref 170 remove cons 263 def 251 remove cons nil cons cons 264 def 105 ref subst 264 remove 157 ref subst 252 remove 146 ref subst 89 ref 91 ref 86 remove 149 remove 243 remove 93 ref appTerm absTerm appTerm appTerm 93 remove appTerm absTerm 265 def 131 remove appTerm 266 def betaConv nil 263 remove 89 ref 239 remove 265 ref appTerm 267 def nil cons 268 def cons nil cons cons nil cons cons 269 def 146 ref subst 241 remove nil 88 ref 238 remove 267 ref appTerm nil cons cons 89 ref 260 remove 267 remove appTerm nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 269 remove 186 remove subst eqMp eqMp nil 88 ref 268 remove cons 89 ref 266 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 247 remove 242 remove 265 remove nil cons cons "x" 2 remove var 250 remove cons nil cons cons nil cons cons 164 ref subst eqMp eqMp eqMp eqMp nil 187 remove 255 remove cons nil cons cons 139 ref subst deductAntisym eqMp eqMp nil 254 remove 127 ref 261 remove cons nil cons cons nil cons cons 139 ref subst deductAntisym eqMp 270 def subst eqMp eqMp proveHyp nil 88 ref 213 remove cons 89 ref 55 remove 30 ref appTerm 271 def nil cons 272 def cons nil cons 273 def cons nil cons cons 146 ref subst nil 215 ref 188 ref 91 ref 224 ref appTerm 271 ref appTerm 274 def absTerm nil cons cons nil cons nil cons cons 219 remove subst 188 remove nil 118 ref 274 remove nil cons cons nil cons nil cons cons 122 ref subst nil 88 ref 224 ref nil cons 275 def cons 273 ref cons nil cons cons 276 def 105 ref subst 276 remove 157 ref subst 225 remove 224 remove assume eqMp nil 88 ref 210 ref nil cons 277 def cons 273 ref cons nil cons cons 278 def 146 ref subst proveHyp 278 ref 105 ref subst 278 remove 157 ref subst "_2226" 1 ref var 279 def "_2227" 1 remove var 280 def 189 remove 280 ref varTerm appTerm 281 def 279 remove varTerm appTerm absTerm absTerm 282 def refl nil 88 ref 33 remove 282 ref appTerm 282 ref appTerm nil cons cons 273 ref cons nil cons cons 146 ref subst proveHyp nil 18 remove 282 ref nil cons cons nil cons nil cons cons nil 88 ref 34 remove 282 ref appTerm 283 def nil cons 284 def cons 273 remove cons nil cons cons 285 def 105 ref subst 285 remove 157 ref subst 38 remove sym 21 ref refl 286 def 60 ref 6 ref 13 ref refl 287 def 283 remove assume 231 ref appThm 282 remove 23 ref appTerm betaConv trans 288 def nil 10 ref 25 ref nil cons cons nil cons nil cons cons 64 ref subst appThm 280 remove 281 remove 23 ref appTerm absTerm 289 def 25 ref appTerm betaConv trans appThm 231 remove appThm absThm appThm appThm 60 ref 6 ref 60 ref 10 ref 287 ref 288 ref 28 ref refl appThm 289 ref 28 ref appTerm betaConv trans appThm 29 ref refl 290 def 288 remove 64 ref appThm 289 remove 27 ref appTerm betaConv trans appThm appThm absThm appThm absThm appThm appThm sym 210 remove assume eqMp eqMp 39 ref 215 remove 30 remove nil cons cons 237 ref 22 remove nil cons cons nil cons cons nil cons cons 256 remove subst proveHyp eqMp nil 126 ref 284 remove cons 127 ref 272 remove cons nil cons 291 def cons nil cons cons 139 ref subst deductAntisym eqMp subst eqMp eqMp nil 126 ref 277 remove cons 291 ref cons nil cons cons 139 ref subst deductAntisym eqMp eqMp eqMp nil 126 ref 275 remove cons 291 ref cons nil cons cons 139 ref subst deductAntisym eqMp eqMp absThm eqMp nil 88 ref 258 remove 237 remove 91 ref 211 remove 259 remove appTerm appTerm 271 ref appTerm absTerm appTerm nil cons cons 89 ref 91 ref 212 remove appTerm 271 remove appTerm nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 39 remove 236 remove 291 remove cons nil cons cons 270 remove subst eqMp eqMp proveHyp eqMp eqMp defineConstList 292 def pop hdTl pop 17 ref constTerm 293 def "Number.Natural.+" const 17 remove constTerm 23 ref appTerm 294 def 27 ref appTerm 295 def appTerm 27 ref appTerm appTerm 23 ref appTerm 296 def absTerm 297 def appTerm 298 def absTerm 299 def nil cons cons nil cons nil cons cons 230 ref subst 6 ref nil 118 ref 298 remove nil cons 300 def cons nil cons nil cons cons 122 ref subst nil 6 ref 294 ref 25 ref appTerm 301 def nil cons cons nil cons nil cons cons 6 ref 13 ref 293 ref 23 ref appTerm 302 def 25 ref appTerm 303 def appTerm 23 ref appTerm absTerm 304 def 23 ref appTerm 305 def betaConv 292 ref nil 126 ref 9 ref 304 ref appTerm nil cons 306 def cons 127 ref 9 ref 6 ref 9 ref 10 ref 13 ref 302 ref 28 ref appTerm 307 def appTerm 29 ref 302 remove 27 ref appTerm 308 def appTerm 309 def appTerm absTerm 310 def appTerm 311 def absTerm 312 def appTerm nil cons 313 def cons nil cons cons nil cons cons 314 def 139 ref subst proveHyp nil 88 ref 306 remove cons 89 ref 305 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 228 ref 5 ref 304 remove nil cons cons 234 ref 23 ref nil cons 315 def cons nil cons 316 def cons nil cons cons 164 ref subst eqMp eqMp 317 def subst 6 ref 13 ref 301 ref appTerm 23 ref appTerm absTerm 318 def 23 ref appTerm 319 def betaConv nil 9 ref 318 ref appTerm 320 def axiom nil 88 ref 320 remove nil cons cons 89 ref 319 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 228 ref 5 ref 318 remove nil cons cons 316 ref cons nil cons cons 164 ref subst eqMp eqMp trans nil 88 ref 13 ref 293 ref 301 remove appTerm 25 ref appTerm appTerm 23 ref appTerm 321 def nil cons cons 89 ref 9 ref 10 ref 91 ref 296 ref appTerm 13 ref 293 ref 294 remove 28 ref appTerm 322 def appTerm 28 ref appTerm appTerm 23 ref appTerm 323 def appTerm 324 def absTerm 325 def appTerm 326 def nil cons cons nil cons cons nil cons cons 157 ref subst proveHyp nil 5 ref 325 remove nil cons cons nil cons nil cons cons 230 ref subst 10 ref nil 118 ref 324 remove nil cons cons nil cons nil cons cons 122 ref subst nil 88 ref 296 ref nil cons 327 def cons 89 ref 323 remove nil cons 328 def cons nil cons cons nil cons cons 329 def 105 ref subst 329 remove 157 ref subst nil 6 ref 322 ref nil cons cons nil cons nil cons cons 310 ref 27 ref appTerm 330 def betaConv 312 ref 23 ref appTerm 331 def betaConv 292 remove 314 remove 232 remove subst proveHyp nil 88 ref 313 remove cons 89 ref 331 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 228 ref 5 ref 312 remove nil cons cons 316 ref cons nil cons cons 164 ref subst eqMp eqMp nil 88 ref 311 remove nil cons cons 89 ref 330 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 228 ref 5 ref 310 remove nil cons cons 235 ref cons nil cons cons 164 ref subst eqMp eqMp 332 def subst 290 ref 293 ref refl 10 ref 13 ref 322 remove appTerm 26 ref 295 ref appTerm appTerm absTerm 333 def 27 ref appTerm 334 def betaConv 6 ref 9 ref 333 ref appTerm 335 def absTerm 336 def 23 ref appTerm 337 def betaConv nil 9 ref 336 ref appTerm 338 def axiom nil 88 ref 338 remove nil cons cons 89 ref 337 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 228 ref 5 ref 336 remove nil cons cons 316 ref cons nil cons cons 164 ref subst eqMp eqMp nil 88 ref 335 remove nil cons cons 89 ref 334 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 228 ref 5 ref 333 remove nil cons cons 235 ref cons nil cons cons 164 ref subst eqMp eqMp appThm 64 remove appThm appThm nil 6 ref 295 remove nil cons cons nil cons nil cons cons 10 ref 13 ref 29 ref 293 remove 26 remove 23 remove appTerm 339 def appTerm 340 def 27 ref appTerm appTerm appTerm 308 remove appTerm 341 def absTerm 342 def 27 ref appTerm 343 def betaConv 344 def 287 ref 290 ref nil 6 remove 339 remove nil cons cons nil cons nil cons cons 345 def 317 ref subst appThm nil 10 ref 315 remove cons nil cons nil cons cons 10 ref 13 ref 29 ref 28 ref appTerm appTerm 27 ref appTerm absTerm 346 def 27 ref appTerm 347 def betaConv nil 9 ref 346 ref appTerm 348 def axiom nil 88 ref 348 remove nil cons cons 89 ref 347 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 228 ref 5 ref 346 remove nil cons cons 235 ref cons nil cons cons 164 ref subst eqMp eqMp subst trans appThm 317 remove appThm nil 316 remove nil cons cons 229 remove nil 118 ref 174 remove 153 remove appTerm nil cons cons nil cons nil cons cons 122 ref subst 163 remove eqMp subst 349 def subst trans sym 121 ref eqMp nil 88 ref 13 ref 29 ref 340 ref 25 ref appTerm appTerm appTerm 303 remove appTerm 350 def nil cons cons 89 ref 9 ref 10 ref 91 ref 341 ref appTerm 13 remove 29 remove 340 remove 28 ref appTerm appTerm appTerm 307 remove appTerm 351 def appTerm 352 def absTerm 353 def appTerm 354 def nil cons cons nil cons cons nil cons cons 157 ref subst proveHyp nil 5 ref 353 remove nil cons cons nil cons nil cons cons 230 remove subst 10 ref nil 118 remove 352 remove nil cons cons nil cons nil cons cons 122 remove subst nil 88 ref 341 ref nil cons 355 def cons 89 ref 351 remove nil cons 356 def cons nil cons cons nil cons cons 357 def 105 remove subst 357 remove 157 remove subst 287 remove 290 remove 345 remove 332 ref subst 341 remove assume trans appThm appThm 332 remove appThm nil 234 remove 309 remove nil cons cons nil cons nil cons cons 349 remove subst trans sym 121 remove eqMp eqMp nil 126 ref 355 remove cons 127 ref 356 remove cons nil cons cons nil cons cons 139 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 88 ref 21 ref 350 remove appTerm 354 remove appTerm nil cons cons 89 ref 9 ref 342 ref appTerm nil cons 358 def cons nil cons cons nil cons cons 146 ref subst proveHyp 91 ref refl 359 def 286 ref 342 ref 25 ref appTerm betaConv appThm 60 ref 10 ref 359 ref 344 ref appThm 342 ref 28 ref appTerm betaConv appThm absThm appThm appThm appThm 60 ref 10 ref 344 remove absThm appThm appThm nil "p" 4 ref var 360 def 342 remove nil cons 361 def cons nil cons nil cons cons 360 ref 91 ref 21 ref 360 ref varTerm 362 def 25 ref appTerm appTerm 9 ref 10 ref 91 remove 362 ref 27 ref appTerm 363 def appTerm 362 ref 28 ref appTerm appTerm absTerm appTerm appTerm appTerm 9 ref 10 ref 363 remove absTerm appTerm appTerm absTerm 364 def 362 ref appTerm 365 def betaConv nil 7 remove 0 remove 8 ref 3 remove cons opType constTerm 364 ref appTerm 366 def axiom nil 88 ref 366 remove nil cons cons 89 ref 365 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp "A" 12 remove cons nil cons "P" 8 remove var 364 remove nil cons cons "x" 4 remove var 362 remove nil cons cons nil cons cons nil cons cons 164 ref subst eqMp eqMp 367 def subst eqMp eqMp nil 88 ref 358 remove cons 89 ref 343 remove nil cons cons nil cons cons nil cons cons 146 ref subst proveHyp 228 remove 5 remove 361 remove cons 235 remove cons nil cons cons 164 remove subst eqMp eqMp subst 296 remove assume trans trans trans eqMp nil 126 remove 327 remove cons 127 remove 328 remove cons nil cons cons nil cons cons 139 remove subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 88 remove 21 remove 321 remove appTerm 326 remove appTerm nil cons cons 89 remove 300 remove cons nil cons cons nil cons cons 146 remove subst proveHyp 359 ref 286 remove 297 ref 25 remove appTerm betaConv appThm 60 ref 10 ref 359 remove 297 ref 27 remove appTerm betaConv 368 def appThm 297 ref 28 remove appTerm betaConv appThm absThm appThm appThm appThm 60 remove 10 remove 368 remove absThm appThm appThm nil 360 remove 297 remove nil cons cons nil cons nil cons cons 367 remove subst eqMp eqMp eqMp absThm eqMp nil 9 remove 299 remove appTerm thm