path: "vendor/opentheory/data/theories/hardware-adder-def/hardware-adder-def.art"
6 version nil "P" "->" typeOp 0 def "Hardware.bus" typeOp nil opType 1 def "bool" typeOp nil opType 2 def nil cons 3 def cons opType 4 def var 5 def "x" 1 ref var 6 def "Data.Bool.!" const 7 def 0 ref 4 ref 3 ref cons opType 8 def constTerm 9 def "y" 1 ref var 10 def 9 ref "s" 1 ref var 11 def 9 ref "c" 1 ref var 12 def "=" const 13 def 0 ref 2 ref 0 ref 2 ref 3 ref cons opType nil cons cons opType 14 def constTerm 15 def "Hardware.Bus.adder2" "_34835" 1 ref var 16 def "_34836" 1 ref var 17 def "_34837" 1 ref var 18 def "_34838" 1 ref var 19 def "Data.Bool./\\" const 14 remove constTerm 20 def "Hardware.Bus.xor2" const 0 ref 1 ref 0 ref 1 ref 4 remove nil cons 21 def cons opType 22 def nil cons cons opType 23 def constTerm 24 def 16 ref varTerm 25 def appTerm 17 ref varTerm 26 def appTerm 18 ref varTerm 27 def appTerm appTerm "Hardware.Bus.and2" const 23 ref constTerm 28 def 25 ref appTerm 26 ref appTerm 19 ref varTerm 29 def appTerm appTerm 30 def absTerm 31 def absTerm 32 def absTerm 33 def absTerm 34 def defineConst 35 def pop 0 ref 1 ref 23 remove nil cons 36 def cons opType 37 def constTerm 38 def 6 ref varTerm 39 def appTerm 10 ref varTerm 40 def appTerm 11 ref varTerm 41 def appTerm 12 ref varTerm 42 def appTerm appTerm 20 ref 24 remove 39 ref appTerm 40 ref appTerm 41 ref appTerm appTerm 28 remove 39 ref appTerm 40 ref appTerm 42 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 43 def nil cons cons nil cons nil cons cons "A" 1 ref nil cons cons nil cons nil nil cons 44 def cons 15 ref 7 ref 0 ref 0 ref "A" varType 45 def 3 ref cons opType 46 def 3 ref cons opType 47 def constTerm 48 def "P" 46 ref var varTerm 49 def appTerm appTerm refl "p" 46 ref var 50 def 13 ref 0 ref 46 remove 47 ref nil cons cons opType constTerm 50 remove varTerm appTerm "x" 45 remove var "Data.Bool.T" const 2 ref constTerm 51 def absTerm appTerm absTerm 52 def 49 ref appTerm betaConv appThm nil 13 ref 0 ref 47 ref 0 ref 47 remove 3 ref cons opType nil cons cons opType constTerm 48 remove appTerm 52 remove appTerm axiom 49 remove refl appThm eqMp sym 53 def subst 54 def subst 16 remove nil "t" 2 remove var 55 def 9 ref 17 ref 9 ref 18 ref 9 ref 19 ref 15 ref 38 ref 25 ref appTerm 26 ref appTerm 27 ref appTerm 29 ref appTerm appTerm 30 remove appTerm 56 def absTerm 57 def appTerm 58 def absTerm 59 def appTerm 60 def absTerm 61 def appTerm nil cons cons nil cons nil cons cons 15 ref 55 ref varTerm 62 def appTerm 51 ref appTerm assume sym nil 51 remove axiom 63 def eqMp 62 remove assume 63 remove deductAntisym deductAntisym 64 def subst nil 5 ref 61 remove nil cons cons nil cons nil cons cons 54 ref subst 17 remove nil 55 ref 60 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 59 remove nil cons cons nil cons nil cons cons 54 ref subst 18 remove nil 55 ref 58 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 57 remove nil cons cons nil cons nil cons cons 54 ref subst 19 remove nil 55 ref 56 remove nil cons cons nil cons nil cons cons 64 ref subst 35 remove 25 ref refl appThm 34 remove 25 remove appTerm betaConv trans 26 ref refl appThm 33 remove 26 remove appTerm betaConv trans 27 ref refl appThm 32 remove 27 remove appTerm betaConv trans 29 ref refl appThm 31 remove 29 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 43 remove appTerm thm nil "P" 0 ref "Hardware.wire" typeOp nil opType 65 def 3 ref cons opType 66 def var 67 def "x" 65 ref var 68 def 7 remove 0 ref 66 ref 3 ref cons opType 69 def constTerm 70 def "y" 65 ref var 71 def 70 ref "s" 65 ref var 72 def 70 ref "c" 65 ref var 73 def 15 ref "Hardware.adder2" "_34758" 65 ref var 74 def "_34759" 65 ref var 75 def "_34760" 65 ref var 76 def "_34761" 65 ref var 77 def 20 ref "Hardware.xor2" const 0 ref 65 ref 0 ref 65 ref 66 remove nil cons 78 def cons opType 79 def nil cons cons opType 80 def constTerm 81 def 74 ref varTerm 82 def appTerm 75 ref varTerm 83 def appTerm 76 ref varTerm 84 def appTerm appTerm "Hardware.and2" const 80 ref constTerm 85 def 82 ref appTerm 83 ref appTerm 77 ref varTerm 86 def appTerm appTerm 87 def absTerm 88 def absTerm 89 def absTerm 90 def absTerm 91 def defineConst 92 def pop 0 ref 65 ref 80 remove nil cons cons opType 93 def constTerm 94 def 68 ref varTerm 95 def appTerm 71 ref varTerm 96 def appTerm 72 ref varTerm 97 def appTerm 73 ref varTerm 98 def appTerm appTerm 20 ref 81 remove 95 ref appTerm 96 ref appTerm 97 ref appTerm appTerm 85 remove 95 ref appTerm 96 ref appTerm 98 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 99 def nil cons cons nil cons nil cons cons "A" 65 ref nil cons cons nil cons 44 remove cons 53 remove subst 100 def subst 74 remove nil 55 ref 70 ref 75 ref 70 ref 76 ref 70 ref 77 ref 15 ref 94 ref 82 ref appTerm 83 ref appTerm 84 ref appTerm 86 ref appTerm appTerm 87 remove appTerm 101 def absTerm 102 def appTerm 103 def absTerm 104 def appTerm 105 def absTerm 106 def appTerm nil cons cons nil cons nil cons cons 64 ref subst nil 67 ref 106 remove nil cons cons nil cons nil cons cons 100 ref subst 75 remove nil 55 ref 105 remove nil cons cons nil cons nil cons cons 64 ref subst nil 67 ref 104 remove nil cons cons nil cons nil cons cons 100 ref subst 76 remove nil 55 ref 103 remove nil cons cons nil cons nil cons cons 64 ref subst nil 67 ref 102 remove nil cons cons nil cons nil cons cons 100 ref subst 77 remove nil 55 ref 101 remove nil cons cons nil cons nil cons cons 64 ref subst 92 remove 82 ref refl appThm 91 remove 82 remove appTerm betaConv trans 83 ref refl appThm 90 remove 83 remove appTerm betaConv trans 84 ref refl appThm 89 remove 84 remove appTerm betaConv trans 86 ref refl appThm 88 remove 86 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 70 ref 99 remove appTerm thm nil 5 ref 6 ref 9 ref 10 ref 9 ref "z" 1 ref var 107 def 9 ref 11 ref 9 ref 12 ref 15 ref "Hardware.Bus.adder3" "_34867" 1 ref var 108 def "_34868" 1 ref var 109 def "_34869" 1 ref var 110 def "_34870" 1 ref var 111 def "_34871" 1 ref var 112 def 20 ref "Hardware.Bus.xor3" const 37 ref constTerm 113 def 108 ref varTerm 114 def appTerm 109 ref varTerm 115 def appTerm 110 ref varTerm 116 def appTerm 111 ref varTerm 117 def appTerm appTerm "Hardware.Bus.majority3" const 37 ref constTerm 118 def 114 ref appTerm 115 ref appTerm 116 ref appTerm 112 ref varTerm 119 def appTerm appTerm 120 def absTerm 121 def absTerm 122 def absTerm 123 def absTerm 124 def absTerm 125 def defineConst 126 def pop 0 ref 1 ref 37 remove nil cons cons opType 127 def constTerm 128 def 39 ref appTerm 40 ref appTerm 107 ref varTerm 129 def appTerm 41 ref appTerm 42 ref appTerm appTerm 20 ref 113 remove 39 ref appTerm 40 ref appTerm 129 ref appTerm 41 ref appTerm appTerm 118 remove 39 ref appTerm 40 ref appTerm 129 ref appTerm 42 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 130 def nil cons cons nil cons nil cons cons 54 ref subst 108 remove nil 55 ref 9 ref 109 ref 9 ref 110 ref 9 ref 111 ref 9 ref 112 ref 15 ref 128 ref 114 ref appTerm 115 ref appTerm 116 ref appTerm 117 ref appTerm 119 ref appTerm appTerm 120 remove appTerm 131 def absTerm 132 def appTerm 133 def absTerm 134 def appTerm 135 def absTerm 136 def appTerm 137 def absTerm 138 def appTerm nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 138 remove nil cons cons nil cons nil cons cons 54 ref subst 109 remove nil 55 ref 137 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 136 remove nil cons cons nil cons nil cons cons 54 ref subst 110 remove nil 55 ref 135 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 134 remove nil cons cons nil cons nil cons cons 54 ref subst 111 remove nil 55 ref 133 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 132 remove nil cons cons nil cons nil cons cons 54 ref subst 112 remove nil 55 ref 131 remove nil cons cons nil cons nil cons cons 64 ref subst 126 remove 114 ref refl appThm 125 remove 114 remove appTerm betaConv trans 115 ref refl appThm 124 remove 115 remove appTerm betaConv trans 116 ref refl appThm 123 remove 116 remove appTerm betaConv trans 117 ref refl appThm 122 remove 117 remove appTerm betaConv trans 119 ref refl appThm 121 remove 119 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 130 remove appTerm thm nil 67 ref 68 remove 70 ref 71 remove 70 ref "z" 65 ref var 139 def 70 ref 72 remove 70 ref 73 remove 15 ref "Hardware.adder3" "_34790" 65 ref var 140 def "_34791" 65 ref var 141 def "_34792" 65 ref var 142 def "_34793" 65 ref var 143 def "_34794" 65 ref var 144 def 20 ref "Hardware.xor3" const 93 ref constTerm 145 def 140 ref varTerm 146 def appTerm 141 ref varTerm 147 def appTerm 142 ref varTerm 148 def appTerm 143 ref varTerm 149 def appTerm appTerm "Hardware.majority3" const 93 ref constTerm 150 def 146 ref appTerm 147 ref appTerm 148 ref appTerm 144 ref varTerm 151 def appTerm appTerm 152 def absTerm 153 def absTerm 154 def absTerm 155 def absTerm 156 def absTerm 157 def defineConst 158 def pop 0 ref 65 ref 93 ref nil cons cons opType constTerm 159 def 95 ref appTerm 96 ref appTerm 139 remove varTerm 160 def appTerm 97 ref appTerm 98 ref appTerm appTerm 20 ref 145 remove 95 ref appTerm 96 ref appTerm 160 ref appTerm 97 remove appTerm appTerm 150 remove 95 remove appTerm 96 remove appTerm 160 remove appTerm 98 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 161 def nil cons cons nil cons nil cons cons 100 ref subst 140 remove nil 55 ref 70 ref 141 ref 70 ref 142 ref 70 ref 143 ref 70 ref 144 ref 15 ref 159 remove 146 ref appTerm 147 ref appTerm 148 ref appTerm 149 ref appTerm 151 ref appTerm appTerm 152 remove appTerm 162 def absTerm 163 def appTerm 164 def absTerm 165 def appTerm 166 def absTerm 167 def appTerm 168 def absTerm 169 def appTerm nil cons cons nil cons nil cons cons 64 ref subst nil 67 ref 169 remove nil cons cons nil cons nil cons cons 100 ref subst 141 remove nil 55 ref 168 remove nil cons cons nil cons nil cons cons 64 ref subst nil 67 ref 167 remove nil cons cons nil cons nil cons cons 100 ref subst 142 remove nil 55 ref 166 remove nil cons cons nil cons nil cons cons 64 ref subst nil 67 ref 165 remove nil cons cons nil cons nil cons cons 100 ref subst 143 remove nil 55 ref 164 remove nil cons cons nil cons nil cons cons 64 ref subst nil 67 ref 163 remove nil cons cons nil cons nil cons cons 100 ref subst 144 remove nil 55 ref 162 remove nil cons cons nil cons nil cons cons 64 ref subst 158 remove 146 ref refl appThm 157 remove 146 remove appTerm betaConv trans 147 ref refl appThm 156 remove 147 remove appTerm betaConv trans 148 ref refl appThm 155 remove 148 remove appTerm betaConv trans 149 ref refl appThm 154 remove 149 remove appTerm betaConv trans 151 ref refl appThm 153 remove 151 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 70 ref 161 remove appTerm thm nil 67 ref "ld" 65 ref var 170 def 9 ref "xs" 1 ref var 171 def 9 ref "xc" 1 ref var 172 def 70 ref "xb" 65 ref var 173 def 15 ref "Hardware.SumCarry.shiftRight" "_34972" 65 ref var 174 def "_34973" 1 ref var 175 def "_34974" 1 ref var 176 def "_34975" 65 ref var 177 def "Data.Bool.?" const 178 def 0 ref 0 ref "Number.Natural.natural" typeOp nil opType 179 def 3 ref cons opType 180 def 3 remove cons opType constTerm 181 def "r" 179 ref var 182 def 178 ref 8 remove constTerm 183 def "sp" 1 ref var 184 def 183 ref "sq" 1 ref var 185 def 183 ref "sr" 1 ref var 186 def 183 ref "cp" 1 ref var 187 def 183 ref "cq" 1 ref var 188 def 183 ref "cr" 1 ref var 189 def 178 remove 69 remove constTerm 190 def "xs0" 65 ref var 191 def 183 ref "xs1" 1 ref var 192 def 190 ref "sq0" 65 ref var 193 def 183 ref "sq1" 1 ref var 194 def 183 ref "sq2" 1 ref var 195 def 190 ref "sq3" 65 ref var 196 def 183 ref "cp0" 1 ref var 197 def 190 ref "cp1" 65 ref var 198 def 183 ref "cq0" 1 ref var 199 def 190 ref "cq1" 65 ref var 200 def 20 ref 13 remove 0 ref 179 ref 180 remove nil cons cons opType constTerm 201 def "Hardware.Bus.width" const 0 ref 1 ref 179 ref nil cons 202 def cons opType constTerm 203 def 175 ref varTerm 204 def appTerm appTerm "Number.Natural.+" const 0 ref 179 ref 0 ref 179 ref 202 remove cons opType 205 def nil cons cons opType constTerm 206 def 182 ref varTerm 207 def appTerm "Number.Natural.bit1" const 205 ref constTerm "Number.Natural.zero" const 179 ref constTerm 208 def appTerm 209 def appTerm 210 def appTerm appTerm 20 ref 201 ref 203 ref 176 ref varTerm 211 def appTerm appTerm 210 ref appTerm appTerm 20 ref 201 ref 203 ref 184 ref varTerm 212 def appTerm appTerm 207 ref appTerm appTerm 213 def 20 ref 201 ref 203 ref 185 ref varTerm 214 def appTerm appTerm 210 ref appTerm appTerm 215 def 20 ref 201 ref 203 ref 186 ref varTerm 216 def appTerm appTerm 207 ref appTerm appTerm 217 def 20 ref 201 ref 203 ref 187 ref varTerm 218 def appTerm appTerm 210 ref appTerm appTerm 219 def 20 ref 201 ref 203 ref 188 ref varTerm 220 def appTerm appTerm 210 ref appTerm appTerm 221 def 20 ref 201 ref 203 ref 189 ref varTerm 222 def appTerm appTerm 210 ref appTerm appTerm 223 def 20 ref "Hardware.Bus.wire" const 0 ref 1 ref 0 ref 179 ref 78 ref cons opType nil cons cons opType constTerm 224 def 204 ref appTerm 208 ref appTerm 191 ref varTerm 225 def appTerm appTerm 20 ref "Hardware.Bus.sub" const 0 ref 1 ref 0 ref 179 ref 0 ref 179 ref 21 remove cons opType nil cons cons opType nil cons cons opType constTerm 226 def 204 ref appTerm 209 ref appTerm 207 ref appTerm 192 ref varTerm 227 def appTerm appTerm 20 ref 224 ref 214 ref appTerm 228 def 208 ref appTerm 193 ref varTerm 229 def appTerm appTerm 230 def 20 ref 226 ref 214 remove appTerm 231 def 208 ref appTerm 207 ref appTerm 194 ref varTerm 232 def appTerm appTerm 233 def 20 ref 231 remove 209 ref appTerm 207 ref appTerm 195 ref varTerm 234 def appTerm appTerm 235 def 20 ref 228 remove 207 ref appTerm 196 ref varTerm 236 def appTerm appTerm 237 def 20 ref 226 ref 218 ref appTerm 208 ref appTerm 207 ref appTerm 197 ref varTerm 238 def appTerm appTerm 239 def 20 ref 224 ref 218 ref appTerm 207 ref appTerm 198 ref varTerm 240 def appTerm appTerm 241 def 20 ref 226 ref 220 ref appTerm 208 ref appTerm 207 ref appTerm 199 ref varTerm 242 def appTerm appTerm 243 def 20 ref 224 ref 220 ref appTerm 207 ref appTerm 200 ref varTerm 244 def appTerm appTerm 245 def 20 ref 38 remove 212 ref appTerm 238 remove appTerm 232 remove appTerm 242 remove appTerm appTerm 246 def 20 ref "Hardware.connect" const 79 remove constTerm 247 def 240 remove appTerm 236 remove appTerm appTerm 248 def 20 ref 247 ref "Hardware.ground" const 65 ref constTerm appTerm 244 remove appTerm appTerm 249 def 20 ref "Hardware.case1" const 93 remove constTerm 250 def 174 ref varTerm 251 def appTerm 225 ref appTerm 229 ref appTerm 177 ref varTerm 252 def appTerm appTerm 20 ref "Hardware.Bus.case1" const 0 ref 65 ref 36 remove cons opType constTerm 253 def 251 ref appTerm 254 def 227 ref appTerm 234 ref appTerm 216 ref appTerm appTerm 20 ref 254 remove 211 ref appTerm 220 ref appTerm 222 ref appTerm appTerm 20 ref "Hardware.Bus.delay" const 22 remove constTerm 255 def 216 ref appTerm 212 remove appTerm appTerm 255 remove 222 ref appTerm 218 remove appTerm appTerm 256 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 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 257 def absTerm 258 def absTerm 259 def absTerm 260 def absTerm 261 def defineConst 262 def pop 0 ref 65 ref 0 ref 1 ref 0 ref 1 ref 78 remove cons opType nil cons cons opType nil cons cons opType constTerm 263 def 170 remove varTerm 264 def appTerm 171 remove varTerm 265 def appTerm 172 remove varTerm 266 def appTerm 173 remove varTerm 267 def appTerm appTerm 181 ref 182 remove 183 ref 184 remove 183 ref 185 remove 183 ref 186 remove 183 ref 187 remove 183 ref 188 remove 183 ref 189 remove 190 ref 191 remove 183 ref 192 remove 190 ref 193 remove 183 ref 194 remove 183 ref 195 remove 190 ref 196 remove 183 ref 197 remove 190 ref 198 remove 183 ref 199 remove 190 ref 200 remove 20 ref 201 ref 203 ref 265 ref appTerm appTerm 210 ref appTerm appTerm 20 ref 201 ref 203 ref 266 ref appTerm appTerm 210 remove appTerm appTerm 213 remove 215 remove 217 remove 219 remove 221 remove 223 remove 20 ref 224 ref 265 ref appTerm 208 ref appTerm 225 ref appTerm appTerm 20 ref 226 ref 265 remove appTerm 209 ref appTerm 207 remove appTerm 227 ref appTerm appTerm 230 remove 233 remove 235 remove 237 remove 239 remove 241 remove 243 remove 245 remove 246 remove 248 remove 249 remove 20 ref 250 remove 264 ref appTerm 225 remove appTerm 229 remove appTerm 267 remove appTerm appTerm 20 ref 253 remove 264 remove appTerm 268 def 227 remove appTerm 234 remove appTerm 216 remove appTerm appTerm 20 ref 268 remove 266 remove appTerm 220 remove appTerm 222 remove appTerm appTerm 256 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 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 269 def nil cons cons nil cons nil cons cons 100 ref subst 174 remove nil 55 ref 9 ref 175 ref 9 ref 176 ref 70 ref 177 ref 15 ref 263 remove 251 ref appTerm 204 ref appTerm 211 ref appTerm 252 ref appTerm appTerm 257 remove appTerm 270 def absTerm 271 def appTerm 272 def absTerm 273 def appTerm 274 def absTerm 275 def appTerm nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 275 remove nil cons cons nil cons nil cons cons 54 ref subst 175 remove nil 55 ref 274 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 273 remove nil cons cons nil cons nil cons cons 54 ref subst 176 remove nil 55 ref 272 remove nil cons cons nil cons nil cons cons 64 ref subst nil 67 remove 271 remove nil cons cons nil cons nil cons cons 100 remove subst 177 remove nil 55 ref 270 remove nil cons cons nil cons nil cons cons 64 ref subst 262 remove 251 ref refl appThm 261 remove 251 remove appTerm betaConv trans 204 ref refl appThm 260 remove 204 remove appTerm betaConv trans 211 ref refl appThm 259 remove 211 remove appTerm betaConv trans 252 ref refl appThm 258 remove 252 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 70 remove 269 remove appTerm thm nil 5 ref "w" 1 ref var 276 def 9 ref 6 remove 9 ref 10 remove 9 ref 107 remove 9 ref 11 remove 9 ref 12 remove 15 ref "Hardware.Bus.adder4" "_34912" 1 ref var 277 def "_34913" 1 ref var 278 def "_34914" 1 ref var 279 def "_34915" 1 ref var 280 def "_34916" 1 ref var 281 def "_34917" 1 ref var 282 def 181 ref "n" 179 remove var 283 def 183 ref "p" 1 ref var 284 def 183 ref "q" 1 ref var 285 def 190 ref "z0" 65 ref var 286 def 183 ref "z1" 1 ref var 287 def 190 ref "s0" 65 ref var 288 def 183 ref "s1" 1 ref var 289 def 190 ref "s2" 65 ref var 290 def 190 ref "c0" 65 ref var 291 def 183 ref "c1" 1 ref var 292 def 190 ref "p0" 65 ref var 293 def 183 ref "p1" 1 ref var 294 def 183 ref "q1" 1 ref var 295 def 190 ref "q2" 65 remove var 296 def 20 ref 201 ref 203 ref 277 ref varTerm 297 def appTerm appTerm 206 remove 283 ref varTerm 298 def appTerm 299 def 209 ref appTerm 300 def appTerm appTerm 20 ref 201 ref 203 ref 278 ref varTerm 301 def appTerm appTerm 300 ref appTerm appTerm 20 ref 201 ref 203 ref 279 ref varTerm 302 def appTerm appTerm 300 ref appTerm appTerm 20 ref 201 ref 203 ref 280 ref varTerm 303 def appTerm appTerm 300 ref appTerm appTerm 20 ref 201 ref 203 ref 281 ref varTerm 304 def appTerm appTerm 299 remove "Number.Natural.bit0" const 205 remove constTerm 209 ref appTerm appTerm 305 def appTerm appTerm 20 ref 201 ref 203 ref 282 ref varTerm 306 def appTerm appTerm 300 ref appTerm appTerm 20 ref 201 ref 203 ref 284 ref varTerm 307 def appTerm appTerm 300 ref appTerm appTerm 308 def 20 ref 201 ref 203 ref 285 ref varTerm 309 def appTerm appTerm 300 ref appTerm appTerm 310 def 20 ref 224 ref 303 ref appTerm 208 ref appTerm 286 ref varTerm 311 def appTerm appTerm 20 ref 226 ref 303 ref appTerm 209 ref appTerm 298 ref appTerm 287 ref varTerm 312 def appTerm appTerm 20 ref 224 ref 304 ref appTerm 313 def 208 ref appTerm 288 ref varTerm 314 def appTerm appTerm 20 ref 226 ref 304 ref appTerm 209 ref appTerm 298 ref appTerm 289 ref varTerm 315 def appTerm appTerm 20 ref 313 remove 300 ref appTerm 290 ref varTerm 316 def appTerm appTerm 20 ref 224 ref 306 ref appTerm 208 ref appTerm 291 ref varTerm 317 def appTerm appTerm 20 ref 226 ref 306 ref appTerm 209 ref appTerm 298 ref appTerm 292 ref varTerm 318 def appTerm appTerm 20 ref 224 ref 307 ref appTerm 208 ref appTerm 293 ref varTerm 319 def appTerm appTerm 320 def 20 ref 226 ref 307 ref appTerm 209 ref appTerm 298 ref appTerm 294 ref varTerm 321 def appTerm appTerm 322 def 20 ref 226 ref 309 ref appTerm 208 ref appTerm 298 ref appTerm 295 ref varTerm 323 def appTerm appTerm 324 def 20 ref 224 ref 309 ref appTerm 298 ref appTerm 296 ref varTerm 325 def appTerm appTerm 326 def 20 ref 128 ref 297 ref appTerm 301 ref appTerm 302 ref appTerm 307 ref appTerm 309 ref appTerm appTerm 20 ref 94 remove 319 remove appTerm 311 ref appTerm 314 ref appTerm 317 ref appTerm appTerm 20 ref 128 ref 321 remove appTerm 323 remove appTerm 312 ref appTerm 315 ref appTerm 318 ref appTerm appTerm 247 remove 325 remove appTerm 316 ref appTerm appTerm appTerm 327 def 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 328 def absTerm 329 def absTerm 330 def absTerm 331 def absTerm 332 def absTerm 333 def absTerm 334 def defineConst 335 def pop 0 remove 1 remove 127 remove nil cons cons opType constTerm 336 def 276 remove varTerm 337 def appTerm 39 ref appTerm 40 ref appTerm 129 ref appTerm 41 ref appTerm 42 ref appTerm appTerm 181 remove 283 remove 183 ref 284 remove 183 ref 285 remove 190 ref 286 remove 183 ref 287 remove 190 ref 288 remove 183 ref 289 remove 190 ref 290 remove 190 ref 291 remove 183 ref 292 remove 190 ref 293 remove 183 ref 294 remove 183 remove 295 remove 190 remove 296 remove 20 ref 201 ref 203 ref 337 ref appTerm appTerm 300 ref appTerm appTerm 20 ref 201 ref 203 ref 39 ref appTerm appTerm 300 ref appTerm appTerm 20 ref 201 ref 203 ref 40 ref appTerm appTerm 300 ref appTerm appTerm 20 ref 201 ref 203 ref 129 ref appTerm appTerm 300 ref appTerm appTerm 20 ref 201 ref 203 ref 41 ref appTerm appTerm 305 remove appTerm appTerm 20 ref 201 remove 203 remove 42 ref appTerm appTerm 300 ref appTerm appTerm 308 remove 310 remove 20 ref 224 ref 129 ref appTerm 208 ref appTerm 311 remove appTerm appTerm 20 ref 226 ref 129 remove appTerm 209 ref appTerm 298 ref appTerm 312 remove appTerm appTerm 20 ref 224 ref 41 ref appTerm 338 def 208 ref appTerm 314 remove appTerm appTerm 20 ref 226 ref 41 remove appTerm 209 ref appTerm 298 ref appTerm 315 remove appTerm appTerm 20 ref 338 remove 300 remove appTerm 316 remove appTerm appTerm 20 ref 224 remove 42 ref appTerm 208 remove appTerm 317 remove appTerm appTerm 20 ref 226 remove 42 remove appTerm 209 remove appTerm 298 remove appTerm 318 remove appTerm appTerm 320 remove 322 remove 324 remove 326 remove 20 remove 128 remove 337 remove appTerm 39 remove appTerm 40 remove appTerm 307 remove appTerm 309 remove appTerm appTerm 327 remove 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 appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 339 def nil cons cons nil cons nil cons cons 54 ref subst 277 remove nil 55 ref 9 ref 278 ref 9 ref 279 ref 9 ref 280 ref 9 ref 281 ref 9 ref 282 ref 15 remove 336 remove 297 ref appTerm 301 ref appTerm 302 ref appTerm 303 ref appTerm 304 ref appTerm 306 ref appTerm appTerm 328 remove appTerm 340 def absTerm 341 def appTerm 342 def absTerm 343 def appTerm 344 def absTerm 345 def appTerm 346 def absTerm 347 def appTerm 348 def absTerm 349 def appTerm nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 349 remove nil cons cons nil cons nil cons cons 54 ref subst 278 remove nil 55 ref 348 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 347 remove nil cons cons nil cons nil cons cons 54 ref subst 279 remove nil 55 ref 346 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 345 remove nil cons cons nil cons nil cons cons 54 ref subst 280 remove nil 55 ref 344 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 ref 343 remove nil cons cons nil cons nil cons cons 54 ref subst 281 remove nil 55 ref 342 remove nil cons cons nil cons nil cons cons 64 ref subst nil 5 remove 341 remove nil cons cons nil cons nil cons cons 54 remove subst 282 remove nil 55 remove 340 remove nil cons cons nil cons nil cons cons 64 remove subst 335 remove 297 ref refl appThm 334 remove 297 remove appTerm betaConv trans 301 ref refl appThm 333 remove 301 remove appTerm betaConv trans 302 ref refl appThm 332 remove 302 remove appTerm betaConv trans 303 ref refl appThm 331 remove 303 remove appTerm betaConv trans 304 ref refl appThm 330 remove 304 remove appTerm betaConv trans 306 ref refl appThm 329 remove 306 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 remove 339 remove appTerm thm