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