path: "vendor/opentheory/data/theories/hardware-multiplier-def/hardware-multiplier-def.art"
6 version nil "P" "->" typeOp 0 def "Hardware.wire" typeOp nil opType 1 def "bool" typeOp nil opType 2 def nil cons 3 def cons opType 4 def var 5 def "ld" 1 ref var 6 def "Data.Bool.!" const 7 def 0 ref 0 ref "Hardware.bus" typeOp nil opType 8 def 3 ref cons opType 9 def 3 ref cons opType 10 def constTerm 11 def "xs" 8 ref var 12 def 11 ref "xc" 8 ref var 13 def 7 ref 0 ref 0 ref "Number.Natural.natural" typeOp nil opType 14 def 3 ref cons opType 15 def 3 ref cons opType 16 def constTerm 17 def "d" 14 ref var 18 def 11 ref "ys" 8 ref var 19 def 11 ref "yc" 8 ref var 20 def 7 ref 0 ref 4 ref 3 ref cons opType 21 def constTerm 22 def "zb" 1 ref var 23 def 11 ref "zs" 8 ref var 24 def 11 ref "zc" 8 ref var 25 def "=" const 26 def 0 ref 2 ref 0 ref 2 ref 3 ref cons opType nil cons cons opType 27 def constTerm 28 def "Hardware.SumCarry.multiplier" "_42573" 1 ref var 29 def "_42574" 8 ref var 30 def "_42575" 8 ref var 31 def "_42576" 14 ref var 32 def "_42577" 8 ref var 33 def "_42578" 8 ref var 34 def "_42579" 1 ref var 35 def "_42580" 8 ref var 36 def "_42581" 8 ref var 37 def "Data.Bool.?" const 38 def 21 remove constTerm 39 def "xb" 1 ref var 40 def 39 ref "ldd" 1 ref var 41 def 39 ref "xbd" 1 ref var 42 def "Data.Bool./\\" const 27 remove constTerm 43 def "Hardware.SumCarry.shiftRight" const 0 ref 1 ref 0 ref 8 ref 0 ref 8 ref 4 remove nil cons 44 def cons opType nil cons cons opType nil cons cons opType constTerm 45 def 29 ref varTerm 46 def appTerm 30 ref varTerm 47 def appTerm 31 ref varTerm 48 def appTerm 40 ref varTerm 49 def appTerm appTerm 43 ref "Hardware.pipe" const 0 ref 1 ref 0 ref 14 ref 44 ref cons opType nil cons 50 def cons opType constTerm 51 def 46 ref appTerm 32 ref varTerm 52 def appTerm 41 ref varTerm 53 def appTerm appTerm 43 ref 51 ref 49 ref appTerm 54 def 52 ref appTerm 42 ref varTerm 55 def appTerm appTerm "Hardware.Bus.multiplier" "_42496" 1 ref var 56 def "_42497" 1 ref var 57 def "_42498" 8 ref var 58 def "_42499" 8 ref var 59 def "_42500" 1 ref var 60 def "_42501" 8 ref var 61 def "_42502" 8 ref var 62 def 38 ref 16 remove constTerm 63 def "r" 14 ref var 64 def 38 remove 10 remove constTerm 65 def "sp" 8 ref var 66 def 65 ref "sq" 8 ref var 67 def 65 ref "sr" 8 ref var 68 def 65 ref "cp" 8 ref var 69 def 65 ref "cq" 8 ref var 70 def 65 ref "cr" 8 ref var 71 def 65 ref "yos" 8 ref var 72 def 65 ref "yoc" 8 ref var 73 def 65 ref "ps" 8 ref var 74 def 65 ref "pc" 8 ref var 75 def 39 ref "sq0" 1 ref var 76 def 65 ref "sq1" 8 ref var 77 def 65 ref "sr0" 8 ref var 78 def 39 ref "sr1" 1 ref var 79 def 65 ref "cq0" 8 ref var 80 def 39 ref "cq1" 1 ref var 81 def 65 ref "cr0" 8 ref var 82 def 39 ref "cr1" 1 ref var 83 def 39 ref "yos0" 1 ref var 84 def 65 ref "yos1" 8 ref var 85 def 65 ref "yoc0" 8 ref var 86 def 39 ref "yoc1" 1 ref var 87 def 39 ref "pc0" 1 ref var 88 def 65 ref "pc1" 8 ref var 89 def 65 ref "pc2" 8 ref var 90 def 39 ref "pc3" 1 ref var 91 def 43 ref 26 ref 0 ref 14 ref 15 ref nil cons cons opType constTerm 92 def "Hardware.Bus.width" const 0 ref 8 ref 14 ref nil cons 93 def cons opType constTerm 94 def 58 ref varTerm 95 def appTerm appTerm "Number.Natural.+" const 0 ref 14 ref 0 ref 14 ref 93 ref cons opType 96 def nil cons cons opType constTerm 64 ref varTerm 97 def appTerm "Number.Natural.bit1" const 96 remove constTerm "Number.Natural.zero" const 14 ref constTerm 98 def appTerm 99 def appTerm 100 def appTerm appTerm 43 ref 92 ref 94 ref 59 ref varTerm 101 def appTerm appTerm 100 ref appTerm appTerm 43 ref 92 ref 94 ref 61 ref varTerm 102 def appTerm appTerm 100 ref appTerm appTerm 43 ref 92 ref 94 ref 62 ref varTerm 103 def appTerm appTerm 100 ref appTerm appTerm 43 ref 92 ref 94 ref 66 ref varTerm 104 def appTerm appTerm 100 ref appTerm appTerm 105 def 43 ref 92 ref 94 ref 67 ref varTerm 106 def appTerm appTerm 100 ref appTerm appTerm 107 def 43 ref 92 ref 94 ref 68 ref varTerm 108 def appTerm appTerm 100 ref appTerm appTerm 109 def 43 ref 92 ref 94 ref 69 ref varTerm 110 def appTerm appTerm 100 ref appTerm appTerm 111 def 43 ref 92 ref 94 ref 70 ref varTerm 112 def appTerm appTerm 100 ref appTerm appTerm 113 def 43 ref 92 ref 94 ref 71 ref varTerm 114 def appTerm appTerm 100 ref appTerm appTerm 115 def 43 ref 92 ref 94 ref 72 ref varTerm 116 def appTerm appTerm 100 ref appTerm appTerm 117 def 43 ref 92 ref 94 ref 73 ref varTerm 118 def appTerm appTerm 100 ref appTerm appTerm 119 def 43 ref 92 ref 94 ref 74 ref varTerm 120 def appTerm appTerm 97 ref appTerm appTerm 121 def 43 ref 92 ref 94 ref 75 ref varTerm 122 def appTerm appTerm 100 ref appTerm appTerm 123 def 43 ref "Hardware.Bus.wire" const 0 ref 8 ref 50 remove cons opType constTerm 124 def 106 ref appTerm 98 ref appTerm 76 ref varTerm 125 def appTerm appTerm 126 def 43 ref "Hardware.Bus.sub" const 0 ref 8 ref 0 ref 14 ref 0 ref 14 ref 9 ref nil cons 127 def cons opType nil cons cons opType nil cons cons opType constTerm 128 def 106 ref appTerm 99 ref appTerm 97 ref appTerm 77 ref varTerm 129 def appTerm appTerm 130 def 43 ref 128 ref 108 ref appTerm 98 ref appTerm 97 ref appTerm 78 ref varTerm 131 def appTerm appTerm 132 def 43 ref 124 ref 108 ref appTerm 97 ref appTerm 79 ref varTerm 133 def appTerm appTerm 134 def 43 ref 128 ref 112 ref appTerm 98 ref appTerm 97 ref appTerm 80 ref varTerm 135 def appTerm appTerm 136 def 43 ref 124 ref 112 ref appTerm 97 ref appTerm 81 ref varTerm 137 def appTerm appTerm 138 def 43 ref 128 ref 114 ref appTerm 98 ref appTerm 97 ref appTerm 82 ref varTerm 139 def appTerm appTerm 140 def 43 ref 124 ref 114 ref appTerm 97 ref appTerm 83 ref varTerm 141 def appTerm appTerm 142 def 43 ref 124 ref 116 ref appTerm 98 ref appTerm 84 ref varTerm 143 def appTerm appTerm 144 def 43 ref 128 ref 116 ref appTerm 99 ref appTerm 97 ref appTerm 85 ref varTerm 145 def appTerm appTerm 146 def 43 ref 128 ref 118 ref appTerm 98 ref appTerm 97 ref appTerm 86 ref varTerm 147 def appTerm appTerm 148 def 43 ref 124 ref 118 ref appTerm 97 ref appTerm 87 ref varTerm 149 def appTerm appTerm 150 def 43 ref 124 remove 122 ref appTerm 151 def 98 ref appTerm 88 ref varTerm 152 def appTerm appTerm 153 def 43 ref 128 remove 122 remove appTerm 154 def 98 remove appTerm 97 ref appTerm 89 ref varTerm 155 def appTerm appTerm 156 def 43 ref 154 remove 99 remove appTerm 97 ref appTerm 90 ref varTerm 157 def appTerm appTerm 158 def 43 ref 151 remove 97 remove appTerm 91 ref varTerm 159 def appTerm appTerm 160 def 43 ref "Hardware.Bus.case1" const 0 ref 1 ref 0 ref 8 ref 0 ref 8 ref 127 remove cons opType 161 def nil cons 162 def cons opType nil cons 163 def cons opType constTerm 164 def 56 ref varTerm 165 def appTerm "Hardware.Bus.ground" const 0 ref 14 ref 8 ref nil cons 166 def cons opType constTerm 100 ref appTerm 167 def appTerm 168 def 104 ref appTerm 106 ref appTerm appTerm 43 ref 168 remove 110 ref appTerm 112 ref appTerm appTerm 43 ref 164 ref 57 ref varTerm 169 def appTerm 170 def 95 ref appTerm 167 ref appTerm 116 ref appTerm appTerm 43 ref 170 remove 101 ref appTerm 167 ref appTerm 118 ref appTerm appTerm 43 ref "Hardware.adder2" const 0 ref 1 ref 0 ref 1 ref 0 ref 1 ref 44 remove cons opType nil cons cons opType nil cons cons opType 171 def constTerm 125 remove appTerm 143 remove appTerm 172 def 60 ref varTerm 173 def appTerm 152 ref appTerm appTerm 43 ref "Hardware.Bus.adder3" const 0 ref 8 ref 0 ref 8 ref 163 remove cons opType nil cons cons opType constTerm 174 def 129 remove appTerm 135 remove appTerm 145 remove appTerm 120 ref appTerm 157 remove appTerm appTerm 175 def 43 ref 174 remove 147 remove appTerm 120 remove appTerm 155 remove appTerm 131 remove appTerm 139 remove appTerm appTerm 176 def 43 ref "Hardware.adder3" const 0 ref 1 ref 171 remove nil cons cons opType constTerm 149 remove appTerm 137 remove appTerm 159 remove appTerm 133 remove appTerm 141 remove appTerm appTerm 177 def 43 ref "Hardware.Bus.connect" const 161 ref constTerm 178 def 108 ref appTerm 179 def 102 ref appTerm appTerm 43 ref 178 remove 114 ref appTerm 180 def 103 ref appTerm appTerm 43 ref "Hardware.Bus.delay" const 161 remove constTerm 181 def 108 remove appTerm 104 ref appTerm appTerm 181 remove 114 remove appTerm 110 ref appTerm appTerm 182 def appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 183 def absTerm 184 def absTerm 185 def absTerm 186 def absTerm 187 def absTerm 188 def absTerm 189 def absTerm 190 def defineConst 191 def pop 0 ref 1 ref 0 ref 1 ref 0 ref 8 ref 0 ref 8 ref 0 ref 1 ref 162 remove cons opType nil cons cons opType nil cons cons opType nil cons 192 def cons opType nil cons cons opType constTerm 193 def 53 ref appTerm 55 ref appTerm 194 def 33 ref varTerm 195 def appTerm 34 ref varTerm 196 def appTerm 35 ref varTerm 197 def appTerm 36 ref varTerm 198 def appTerm 37 ref varTerm 199 def appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 200 def absTerm 201 def absTerm 202 def absTerm 203 def absTerm 204 def absTerm 205 def absTerm 206 def absTerm 207 def absTerm 208 def absTerm 209 def defineConst 210 def pop 0 ref 1 ref 0 ref 8 ref 0 ref 8 remove 0 ref 14 remove 192 remove cons opType nil cons cons opType nil cons cons opType nil cons cons opType constTerm 211 def 6 ref varTerm 212 def appTerm 12 remove varTerm 213 def appTerm 13 remove varTerm 214 def appTerm 18 remove varTerm 215 def appTerm 19 ref varTerm 216 def appTerm 20 ref varTerm 217 def appTerm 23 ref varTerm 218 def appTerm 24 ref varTerm 219 def appTerm 25 ref varTerm 220 def appTerm appTerm 39 ref 40 ref 39 ref 41 remove 39 ref 42 remove 43 ref 45 remove 212 ref appTerm 213 remove appTerm 214 remove appTerm 49 ref appTerm appTerm 43 ref 51 remove 212 ref appTerm 215 ref appTerm 53 remove appTerm appTerm 43 ref 54 remove 215 remove appTerm 55 remove appTerm appTerm 194 remove 216 ref appTerm 217 ref appTerm 218 ref appTerm 219 ref appTerm 220 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 221 def nil cons cons nil cons nil cons cons "A" 1 remove nil cons cons nil cons nil nil cons 222 def cons 28 ref 7 remove 0 ref 0 ref "A" varType 223 def 3 ref cons opType 224 def 3 ref cons opType 225 def constTerm 226 def "P" 224 ref var varTerm 227 def appTerm appTerm refl "p" 224 ref var 228 def 26 ref 0 ref 224 remove 225 ref nil cons cons opType constTerm 228 remove varTerm appTerm "x" 223 remove var "Data.Bool.T" const 2 ref constTerm 229 def absTerm appTerm absTerm 230 def 227 ref appTerm betaConv appThm nil 26 remove 0 ref 225 ref 0 remove 225 remove 3 remove cons opType nil cons cons opType constTerm 226 remove appTerm 230 remove appTerm axiom 227 remove refl appThm eqMp sym 231 def subst 232 def subst 29 remove nil "t" 2 remove var 233 def 11 ref 30 ref 11 ref 31 ref 17 remove 32 ref 11 ref 33 ref 11 ref 34 ref 22 ref 35 ref 11 ref 36 ref 11 ref 37 ref 28 ref 211 remove 46 ref appTerm 47 ref appTerm 48 ref appTerm 52 ref appTerm 195 ref appTerm 196 ref appTerm 197 ref appTerm 198 ref appTerm 199 ref appTerm appTerm 200 remove appTerm 234 def absTerm 235 def appTerm 236 def absTerm 237 def appTerm 238 def absTerm 239 def 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 nil cons cons nil cons nil cons cons 28 ref 233 ref varTerm 250 def appTerm 229 ref appTerm assume sym nil 229 remove axiom 251 def eqMp 250 remove assume 251 remove deductAntisym deductAntisym 252 def subst nil "P" 9 remove var 253 def 249 remove nil cons cons nil cons nil cons cons "A" 166 remove cons nil cons 222 ref cons 231 ref subst 254 def subst 30 remove nil 233 ref 248 remove nil cons cons nil cons nil cons cons 252 ref subst nil 253 ref 247 remove nil cons cons nil cons nil cons cons 254 ref subst 31 remove nil 233 ref 246 remove nil cons cons nil cons nil cons cons 252 ref subst nil "P" 15 remove var 245 remove nil cons cons nil cons nil cons cons "A" 93 remove cons nil cons 222 remove cons 231 remove subst subst 32 remove nil 233 ref 244 remove nil cons cons nil cons nil cons cons 252 ref subst nil 253 ref 243 remove nil cons cons nil cons nil cons cons 254 ref subst 33 remove nil 233 ref 242 remove nil cons cons nil cons nil cons cons 252 ref subst nil 253 ref 241 remove nil cons cons nil cons nil cons cons 254 ref subst 34 remove nil 233 ref 240 remove nil cons cons nil cons nil cons cons 252 ref subst nil 5 ref 239 remove nil cons cons nil cons nil cons cons 232 ref subst 35 remove nil 233 ref 238 remove nil cons cons nil cons nil cons cons 252 ref subst nil 253 ref 237 remove nil cons cons nil cons nil cons cons 254 ref subst 36 remove nil 233 ref 236 remove nil cons cons nil cons nil cons cons 252 ref subst nil 253 ref 235 remove nil cons cons nil cons nil cons cons 254 ref subst 37 remove nil 233 ref 234 remove nil cons cons nil cons nil cons cons 252 ref subst 210 remove 46 ref refl appThm 209 remove 46 remove appTerm betaConv trans 47 ref refl appThm 208 remove 47 remove appTerm betaConv trans 48 ref refl appThm 207 remove 48 remove appTerm betaConv trans 52 ref refl appThm 206 remove 52 remove appTerm betaConv trans 195 ref refl appThm 205 remove 195 remove appTerm betaConv trans 196 ref refl appThm 204 remove 196 remove appTerm betaConv trans 197 ref refl appThm 203 remove 197 remove appTerm betaConv trans 198 ref refl appThm 202 remove 198 remove appTerm betaConv trans 199 ref refl appThm 201 remove 199 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 22 ref 221 remove appTerm thm nil 5 ref 6 remove 22 ref 40 remove 11 ref 19 remove 11 ref 20 remove 22 ref 23 remove 11 ref 24 remove 11 ref 25 remove 28 ref 193 ref 212 ref appTerm 49 ref appTerm 216 ref appTerm 217 ref appTerm 218 ref appTerm 219 ref appTerm 220 ref appTerm appTerm 63 remove 64 remove 65 ref 66 remove 65 ref 67 remove 65 ref 68 remove 65 ref 69 remove 65 ref 70 remove 65 ref 71 remove 65 ref 72 remove 65 ref 73 remove 65 ref 74 remove 65 ref 75 remove 39 ref 76 remove 65 ref 77 remove 65 ref 78 remove 39 ref 79 remove 65 ref 80 remove 39 ref 81 remove 65 ref 82 remove 39 ref 83 remove 39 ref 84 remove 65 ref 85 remove 65 ref 86 remove 39 ref 87 remove 39 ref 88 remove 65 ref 89 remove 65 remove 90 remove 39 remove 91 remove 43 ref 92 ref 94 ref 216 ref appTerm appTerm 100 ref appTerm appTerm 43 ref 92 ref 94 ref 217 ref appTerm appTerm 100 ref appTerm appTerm 43 ref 92 ref 94 ref 219 ref appTerm appTerm 100 ref appTerm appTerm 43 ref 92 remove 94 remove 220 ref appTerm appTerm 100 remove appTerm appTerm 105 remove 107 remove 109 remove 111 remove 113 remove 115 remove 117 remove 119 remove 121 remove 123 remove 126 remove 130 remove 132 remove 134 remove 136 remove 138 remove 140 remove 142 remove 144 remove 146 remove 148 remove 150 remove 153 remove 156 remove 158 remove 160 remove 43 ref 164 ref 212 remove appTerm 167 ref appTerm 255 def 104 remove appTerm 106 remove appTerm appTerm 43 ref 255 remove 110 remove appTerm 112 remove appTerm appTerm 43 ref 164 remove 49 remove appTerm 256 def 216 remove appTerm 167 ref appTerm 116 remove appTerm appTerm 43 ref 256 remove 217 remove appTerm 167 remove appTerm 118 remove appTerm appTerm 43 ref 172 remove 218 remove appTerm 152 remove appTerm appTerm 175 remove 176 remove 177 remove 43 ref 179 remove 219 remove appTerm appTerm 43 remove 180 remove 220 remove appTerm appTerm 182 remove appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 257 def nil cons cons nil cons nil cons cons 232 ref subst 56 remove nil 233 ref 22 ref 57 ref 11 ref 58 ref 11 ref 59 ref 22 ref 60 ref 11 ref 61 ref 11 remove 62 ref 28 remove 193 remove 165 ref appTerm 169 ref appTerm 95 ref appTerm 101 ref appTerm 173 ref appTerm 102 ref appTerm 103 ref appTerm appTerm 183 remove appTerm 258 def absTerm 259 def appTerm 260 def absTerm 261 def appTerm 262 def absTerm 263 def appTerm 264 def absTerm 265 def appTerm 266 def absTerm 267 def appTerm 268 def absTerm 269 def appTerm nil cons cons nil cons nil cons cons 252 ref subst nil 5 ref 269 remove nil cons cons nil cons nil cons cons 232 ref subst 57 remove nil 233 ref 268 remove nil cons cons nil cons nil cons cons 252 ref subst nil 253 ref 267 remove nil cons cons nil cons nil cons cons 254 ref subst 58 remove nil 233 ref 266 remove nil cons cons nil cons nil cons cons 252 ref subst nil 253 ref 265 remove nil cons cons nil cons nil cons cons 254 ref subst 59 remove nil 233 ref 264 remove nil cons cons nil cons nil cons cons 252 ref subst nil 5 remove 263 remove nil cons cons nil cons nil cons cons 232 remove subst 60 remove nil 233 ref 262 remove nil cons cons nil cons nil cons cons 252 ref subst nil 253 ref 261 remove nil cons cons nil cons nil cons cons 254 ref subst 61 remove nil 233 ref 260 remove nil cons cons nil cons nil cons cons 252 ref subst nil 253 remove 259 remove nil cons cons nil cons nil cons cons 254 remove subst 62 remove nil 233 remove 258 remove nil cons cons nil cons nil cons cons 252 remove subst 191 remove 165 ref refl appThm 190 remove 165 remove appTerm betaConv trans 169 ref refl appThm 189 remove 169 remove appTerm betaConv trans 95 ref refl appThm 188 remove 95 remove appTerm betaConv trans 101 ref refl appThm 187 remove 101 remove appTerm betaConv trans 173 ref refl appThm 186 remove 173 remove appTerm betaConv trans 102 ref refl appThm 185 remove 102 remove appTerm betaConv trans 103 ref refl appThm 184 remove 103 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 22 remove 257 remove appTerm thm