path: "vendor/opentheory/data/theories/hardware-counter-def/hardware-counter-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 "nb" 8 ref var 12 def 7 ref 0 ref 4 ref 3 ref cons opType 13 def constTerm 14 def "dn" 1 ref var 15 def "=" const 16 def 0 ref 2 ref 0 ref 2 ref 3 ref cons opType nil cons cons opType 17 def constTerm 18 def "Hardware.counterPulse" "_35436" 1 ref var 19 def "_35437" 8 ref var 20 def "_35438" 1 ref var 21 def "Data.Bool.?" const 22 def 13 remove constTerm 23 def "ds" 1 ref var 24 def "Data.Bool./\\" const 17 remove constTerm 25 def "Hardware.counter" "_35415" 1 ref var 26 def "_35416" 8 ref var 27 def "_35417" 1 ref var 28 def 22 ref 0 ref 0 ref "Number.Natural.natural" typeOp nil opType 29 def 3 ref cons opType 30 def 3 ref cons opType 31 def constTerm 32 def "r" 29 ref var 33 def 22 remove 10 remove constTerm 34 def "sp" 8 ref var 35 def 34 ref "cp" 8 ref var 36 def 34 ref "sq" 8 ref var 37 def 34 ref "cq" 8 ref var 38 def 34 ref "sr" 8 ref var 39 def 34 ref "cr" 8 ref var 40 def 23 ref "dp" 1 ref var 41 def 23 ref "dq" 1 ref var 42 def 23 ref "dr" 1 ref var 43 def 23 ref "nb0" 1 ref var 44 def 34 ref "nb1" 8 ref var 45 def 23 ref "cp0" 1 ref var 46 def 34 ref "cp1" 8 ref var 47 def 23 ref "cp2" 1 ref var 48 def 23 ref "cq0" 1 ref var 49 def 34 ref "cq1" 8 ref var 50 def 23 ref "cr0" 1 ref var 51 def 34 ref "cr1" 8 ref var 52 def 25 ref 16 ref 0 ref 29 ref 30 ref nil cons cons opType constTerm 53 def "Hardware.Bus.width" const 0 ref 8 ref 29 ref nil cons 54 def cons opType constTerm 55 def 27 ref varTerm 56 def appTerm appTerm "Number.Natural.+" const 0 ref 29 ref 0 ref 29 ref 54 ref cons opType 57 def nil cons cons opType constTerm 58 def 33 ref varTerm 59 def appTerm "Number.Natural.bit1" const 57 remove constTerm "Number.Natural.zero" const 29 ref constTerm 60 def appTerm 61 def appTerm 62 def appTerm appTerm 25 ref 53 ref 55 ref 35 ref varTerm 63 def appTerm appTerm 64 def 59 ref appTerm appTerm 65 def 25 ref 53 ref 55 ref 36 ref varTerm 66 def appTerm appTerm 62 ref appTerm appTerm 67 def 25 ref 53 ref 55 ref 37 ref varTerm 68 def appTerm appTerm 69 def 59 ref appTerm appTerm 70 def 25 ref 53 ref 55 ref 38 ref varTerm 71 def appTerm appTerm 62 ref appTerm appTerm 72 def 25 ref 53 ref 55 ref 39 ref varTerm 73 def appTerm appTerm 74 def 59 ref appTerm appTerm 75 def 25 ref 53 ref 55 ref 40 ref varTerm 76 def appTerm appTerm 62 ref appTerm appTerm 77 def 25 ref "Hardware.Bus.wire" const 0 ref 8 ref 0 ref 29 ref 4 remove nil cons 78 def cons opType nil cons 79 def cons opType constTerm 80 def 56 ref appTerm 60 ref appTerm 44 ref varTerm 81 def appTerm appTerm 25 ref "Hardware.Bus.sub" const 0 ref 8 ref 0 ref 29 ref 0 ref 29 ref 9 ref nil cons 82 def cons opType nil cons cons opType nil cons cons opType constTerm 83 def 56 ref appTerm 61 ref appTerm 59 ref appTerm 45 ref varTerm 84 def appTerm appTerm 25 ref 80 ref 66 ref appTerm 85 def 60 ref appTerm 46 ref varTerm 86 def appTerm appTerm 87 def 25 ref 83 ref 66 ref appTerm 60 ref appTerm 59 ref appTerm 47 ref varTerm 88 def appTerm appTerm 89 def 25 ref 85 remove 59 ref appTerm 48 ref varTerm 90 def appTerm appTerm 91 def 25 ref 80 ref 71 ref appTerm 60 ref appTerm 49 ref varTerm 92 def appTerm appTerm 93 def 25 ref 83 ref 71 ref appTerm 61 ref appTerm 59 ref appTerm 50 ref varTerm 94 def appTerm appTerm 95 def 25 ref 80 ref 76 ref appTerm 60 ref appTerm 51 ref varTerm 96 def appTerm appTerm 97 def 25 ref 83 ref 76 ref appTerm 61 ref appTerm 59 ref appTerm 52 ref varTerm 98 def appTerm appTerm 99 def 25 ref "Hardware.not" const 0 ref 1 ref 78 ref cons opType 100 def constTerm 86 remove appTerm 92 ref appTerm appTerm 101 def 25 ref "Hardware.Bus.adder2" const 0 ref 8 ref 0 ref 8 ref 0 ref 8 ref 82 ref cons opType 102 def nil cons cons opType nil cons 103 def cons opType constTerm 104 def 63 ref appTerm 88 ref appTerm 68 ref appTerm 94 ref appTerm appTerm 105 def 25 ref "Hardware.or2" const 0 ref 1 ref 100 ref nil cons 106 def cons opType 107 def constTerm 41 ref varTerm 108 def appTerm 90 remove appTerm 42 ref varTerm 109 def appTerm appTerm 110 def 25 ref "Hardware.Bus.case1" const 0 ref 1 ref 103 remove cons opType constTerm 111 def 26 ref varTerm 112 def appTerm 113 def 84 ref appTerm 68 ref appTerm 73 ref appTerm appTerm 25 ref "Hardware.case1" const 0 ref 1 ref 107 ref nil cons cons opType constTerm 114 def 112 ref appTerm 115 def 81 ref appTerm 92 ref appTerm 96 ref appTerm appTerm 25 ref 113 remove "Hardware.Bus.ground" const 0 ref 29 ref 8 ref nil cons 116 def cons opType constTerm 117 def 59 ref appTerm 118 def appTerm 94 ref appTerm 98 ref appTerm appTerm 25 ref 115 remove "Hardware.ground" const 1 ref constTerm 119 def appTerm 109 ref appTerm 43 ref varTerm 120 def appTerm appTerm 25 ref "Hardware.connect" const 100 ref constTerm 121 def 120 ref appTerm 122 def 28 ref varTerm 123 def appTerm appTerm 25 ref "Hardware.Bus.delay" const 102 ref constTerm 124 def 73 ref appTerm 63 ref appTerm appTerm 25 ref 124 ref 76 ref appTerm 66 remove appTerm appTerm "Hardware.delay" const 100 ref constTerm 120 ref appTerm 108 remove appTerm appTerm appTerm 125 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 absTerm appTerm absTerm appTerm 126 def absTerm 127 def absTerm 128 def absTerm 129 def defineConst 130 def pop 0 ref 1 ref 0 ref 8 ref 78 remove cons opType nil cons cons opType 131 def constTerm 132 def 19 ref varTerm 133 def appTerm 20 ref varTerm 134 def appTerm 24 ref varTerm 135 def appTerm appTerm "Hardware.pulse" const 100 remove constTerm 135 ref appTerm 136 def 21 ref varTerm 137 def appTerm appTerm absTerm appTerm 138 def absTerm 139 def absTerm 140 def absTerm 141 def defineConst 142 def pop 131 remove constTerm 143 def 6 ref varTerm 144 def appTerm 12 ref varTerm 145 def appTerm 15 ref varTerm 146 def appTerm appTerm 23 ref 24 remove 25 ref 132 ref 144 ref appTerm 145 ref appTerm 147 def 135 remove appTerm appTerm 136 remove 146 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 148 def nil cons cons nil cons nil cons cons "A" 1 ref nil cons cons nil cons nil nil cons 149 def cons 18 ref 7 ref 0 ref 0 ref "A" varType 150 def 3 ref cons opType 151 def 3 ref cons opType 152 def constTerm 153 def "P" 151 ref var varTerm 154 def appTerm appTerm refl "p" 151 ref var 155 def 16 ref 0 ref 151 remove 152 ref nil cons cons opType constTerm 155 remove varTerm appTerm "x" 150 remove var "Data.Bool.T" const 2 ref constTerm 156 def absTerm appTerm absTerm 157 def 154 ref appTerm betaConv appThm nil 16 remove 0 ref 152 ref 0 ref 152 remove 3 remove cons opType nil cons cons opType constTerm 153 remove appTerm 157 remove appTerm axiom 154 remove refl appThm eqMp sym 158 def subst 159 def subst 19 remove nil "t" 2 remove var 160 def 11 ref 20 ref 14 ref 21 ref 18 ref 143 remove 133 ref appTerm 134 ref appTerm 137 ref appTerm appTerm 138 remove appTerm 161 def absTerm 162 def appTerm 163 def absTerm 164 def appTerm nil cons cons nil cons nil cons cons 18 ref 160 ref varTerm 165 def appTerm 156 ref appTerm assume sym nil 156 remove axiom 166 def eqMp 165 remove assume 166 remove deductAntisym deductAntisym 167 def subst nil "P" 9 remove var 168 def 164 remove nil cons cons nil cons nil cons cons "A" 116 remove cons nil cons 149 ref cons 158 ref subst 169 def subst 20 remove nil 160 ref 163 remove nil cons cons nil cons nil cons cons 167 ref subst nil 5 ref 162 remove nil cons cons nil cons nil cons cons 159 ref subst 21 remove nil 160 ref 161 remove nil cons cons nil cons nil cons cons 167 ref subst 142 remove 133 ref refl appThm 141 remove 133 remove appTerm betaConv trans 134 ref refl appThm 140 remove 134 remove appTerm betaConv trans 137 ref refl appThm 139 remove 137 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 14 ref 148 remove appTerm thm nil 5 ref "w" 1 ref var 170 def 7 remove 31 remove constTerm 171 def "d" 29 ref var 172 def 14 ref "wd" 1 ref var 173 def 18 ref "Hardware.pipe" "_35362" 1 ref var 174 def "_35363" 29 remove var 175 def "_35364" 1 ref var 176 def 34 ref "x" 8 ref var 177 def 23 ref "x0" 1 ref var 178 def 25 ref 53 ref 55 ref 177 ref varTerm 179 def appTerm appTerm 180 def 58 ref 175 ref varTerm 181 def appTerm 61 ref appTerm appTerm appTerm 25 ref 80 ref 179 ref appTerm 182 def 181 ref appTerm 178 ref varTerm 183 def appTerm appTerm 25 ref "Hardware.Bus.pipe" "_35350" 1 ref var 184 def "_35351" 8 ref var 185 def 32 ref 33 ref 34 ref "xp" 8 ref var 186 def 23 ref 178 ref 34 ref "x1" 8 ref var 187 def 34 ref "x2" 8 ref var 188 def 25 ref 53 ref 55 ref 185 ref varTerm 189 def appTerm appTerm 62 ref appTerm appTerm 25 ref 53 ref 55 ref 186 ref varTerm 190 def appTerm appTerm 59 ref appTerm appTerm 191 def 25 ref 80 ref 189 ref appTerm 60 ref appTerm 183 ref appTerm appTerm 25 ref 83 ref 189 ref appTerm 192 def 60 ref appTerm 59 ref appTerm 187 ref varTerm 193 def appTerm appTerm 25 ref 192 remove 61 ref appTerm 59 ref appTerm 188 ref varTerm 194 def appTerm appTerm 25 ref 121 ref 184 ref varTerm 195 def appTerm 183 ref appTerm appTerm 25 ref "Hardware.Bus.connect" const 102 remove constTerm 190 ref appTerm 194 ref appTerm appTerm 124 remove 193 ref appTerm 190 remove appTerm appTerm 196 def appTerm appTerm appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 197 def absTerm 198 def absTerm 199 def defineConst 200 def pop 0 ref 1 ref 82 remove cons opType constTerm 201 def 174 ref varTerm 202 def appTerm 179 ref appTerm appTerm 121 ref 183 ref appTerm 203 def 176 ref varTerm 204 def appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm 205 def absTerm 206 def absTerm 207 def absTerm 208 def defineConst 209 def pop 0 ref 1 ref 79 remove cons opType constTerm 210 def 170 ref varTerm 211 def appTerm 172 remove varTerm 212 def appTerm 173 remove varTerm 213 def appTerm appTerm 34 ref 177 ref 23 ref 178 ref 25 ref 180 ref 58 remove 212 ref appTerm 61 ref appTerm appTerm appTerm 25 ref 182 ref 212 remove appTerm 183 ref appTerm appTerm 25 ref 201 ref 211 ref appTerm 179 ref appTerm 214 def appTerm 203 remove 213 remove appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 215 def nil cons cons nil cons nil cons cons 159 ref subst 174 remove nil 160 ref 171 remove 175 ref 14 ref 176 ref 18 ref 210 remove 202 ref appTerm 181 ref appTerm 204 ref appTerm appTerm 205 remove appTerm 216 def absTerm 217 def appTerm 218 def absTerm 219 def appTerm nil cons cons nil cons nil cons cons 167 ref subst nil "P" 30 remove var 219 remove nil cons cons nil cons nil cons cons "A" 54 remove cons nil cons 149 remove cons 158 remove subst subst 175 remove nil 160 ref 218 remove nil cons cons nil cons nil cons cons 167 ref subst nil 5 ref 217 remove nil cons cons nil cons nil cons cons 159 ref subst 176 remove nil 160 ref 216 remove nil cons cons nil cons nil cons cons 167 ref subst 209 remove 202 ref refl appThm 208 remove 202 remove appTerm betaConv trans 181 ref refl appThm 207 remove 181 remove appTerm betaConv trans 204 ref refl appThm 206 remove 204 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 14 ref 215 remove appTerm thm nil 5 ref 170 remove 11 ref 177 remove 18 ref 214 remove appTerm 32 ref 33 ref 34 ref 186 remove 23 ref 178 remove 34 ref 187 remove 34 ref 188 remove 25 ref 180 remove 62 ref appTerm appTerm 191 remove 25 ref 182 remove 60 ref appTerm 183 ref appTerm appTerm 25 ref 83 ref 179 remove appTerm 220 def 60 ref appTerm 59 ref appTerm 193 remove appTerm appTerm 25 ref 220 remove 61 ref appTerm 59 ref appTerm 194 remove appTerm appTerm 25 ref 121 remove 211 remove appTerm 183 remove appTerm appTerm 196 remove appTerm appTerm appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm 221 def nil cons cons nil cons nil cons cons 159 ref subst 184 remove nil 160 ref 11 ref 185 ref 18 ref 201 remove 195 ref appTerm 189 ref appTerm appTerm 197 remove appTerm 222 def absTerm 223 def appTerm nil cons cons nil cons nil cons cons 167 ref subst nil 168 ref 223 remove nil cons cons nil cons nil cons cons 169 ref subst 185 remove nil 160 ref 222 remove nil cons cons nil cons nil cons cons 167 ref subst 200 remove 195 ref refl appThm 199 remove 195 remove appTerm betaConv trans 189 ref refl appThm 198 remove 189 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 14 ref 221 remove appTerm thm nil 5 ref 6 ref 11 ref 12 ref 14 ref 15 ref 18 ref 147 remove 146 ref appTerm appTerm 32 ref 33 ref 34 ref 35 ref 34 ref 36 ref 34 ref 37 ref 34 ref 38 ref 34 ref 39 ref 34 ref 40 ref 23 ref 41 ref 23 ref 42 ref 23 ref 43 ref 23 ref 44 remove 34 ref 45 remove 23 ref 46 ref 34 ref 47 ref 23 ref 48 ref 23 ref 49 ref 34 ref 50 ref 23 ref 51 remove 34 ref 52 remove 25 ref 53 ref 55 ref 145 ref appTerm appTerm 62 ref appTerm appTerm 224 def 65 remove 67 ref 70 remove 72 ref 75 remove 77 ref 25 ref 80 ref 145 ref appTerm 60 ref appTerm 81 ref appTerm appTerm 25 ref 83 ref 145 ref appTerm 61 ref appTerm 59 ref appTerm 84 ref appTerm appTerm 87 ref 89 ref 91 ref 93 ref 95 ref 97 remove 99 remove 101 remove 105 remove 110 ref 25 ref 111 ref 144 ref appTerm 225 def 84 remove appTerm 68 ref appTerm 73 ref appTerm appTerm 25 ref 114 ref 144 ref appTerm 226 def 81 remove appTerm 92 ref appTerm 96 remove appTerm appTerm 25 ref 225 ref 118 remove appTerm 94 ref appTerm 98 remove appTerm appTerm 25 ref 226 remove 119 ref appTerm 109 ref appTerm 120 ref appTerm appTerm 25 ref 122 ref 146 ref appTerm appTerm 125 ref appTerm appTerm 227 def 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 appTerm absTerm appTerm absTerm appTerm absTerm 228 def nil cons cons nil cons nil cons cons 159 ref subst 26 remove nil 160 ref 11 ref 27 ref 14 ref 28 ref 18 ref 132 remove 112 ref appTerm 56 ref appTerm 123 ref appTerm appTerm 126 remove appTerm 229 def absTerm 230 def appTerm 231 def absTerm 232 def appTerm nil cons cons nil cons nil cons cons 167 ref subst nil 168 ref 232 remove nil cons cons nil cons nil cons cons 169 ref subst 27 remove nil 160 ref 231 remove nil cons cons nil cons nil cons cons 167 ref subst nil 5 ref 230 remove nil cons cons nil cons nil cons cons 159 ref subst 28 remove nil 160 ref 229 remove nil cons cons nil cons nil cons cons 167 ref subst 130 remove 112 ref refl appThm 129 remove 112 remove appTerm betaConv trans 56 ref refl appThm 128 remove 56 remove appTerm betaConv trans 123 ref refl appThm 127 remove 123 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 14 ref 228 remove appTerm thm nil 5 ref 6 remove 11 ref 12 remove 14 ref "inc" 1 ref var 233 def 14 ref 15 remove 18 ref "Hardware.eventCounter" "_35383" 1 ref var 234 def "_35384" 8 ref var 235 def "_35385" 1 ref var 236 def "_35386" 1 ref var 237 def 32 ref 33 ref 34 ref 35 ref 34 ref 36 ref 34 ref 37 ref 34 ref 38 ref 34 ref 39 ref 34 ref 40 ref 23 ref 41 ref 23 ref 42 ref 23 ref 43 ref 23 ref "sp0" 1 ref var 238 def 34 ref "sp1" 8 ref var 239 def 23 ref 46 ref 34 ref 47 ref 23 ref 48 ref 23 ref "sq0" 1 ref var 240 def 34 ref "sq1" 8 ref var 241 def 23 ref 49 ref 34 ref 50 ref 25 ref 53 remove 55 remove 235 ref varTerm 242 def appTerm appTerm 62 ref appTerm appTerm 25 ref 64 remove 62 ref appTerm appTerm 243 def 67 ref 25 ref 69 remove 62 ref appTerm appTerm 244 def 72 ref 25 ref 74 remove 62 ref appTerm appTerm 245 def 77 ref 25 ref 80 ref 63 ref appTerm 60 ref appTerm 238 ref varTerm 246 def appTerm appTerm 247 def 25 ref 83 ref 63 remove appTerm 61 ref appTerm 59 ref appTerm 239 ref varTerm 248 def appTerm appTerm 249 def 25 ref 80 remove 68 ref appTerm 60 remove appTerm 240 ref varTerm 250 def appTerm appTerm 251 def 25 ref 83 remove 68 ref appTerm 61 remove appTerm 59 remove appTerm 241 ref varTerm 252 def appTerm appTerm 253 def 87 ref 89 ref 91 ref 93 ref 95 ref 25 ref "Hardware.xor2" const 107 ref constTerm 254 def 236 ref varTerm 255 def appTerm 246 ref appTerm 250 ref appTerm appTerm 25 ref "Hardware.and2" const 107 remove constTerm 256 def 255 ref appTerm 246 ref appTerm 92 ref appTerm appTerm 25 ref 104 remove 248 remove appTerm 88 remove appTerm 252 remove appTerm 94 remove appTerm appTerm 257 def 110 ref 25 ref 111 remove 234 ref varTerm 258 def appTerm 259 def 242 ref appTerm 68 ref appTerm 73 ref appTerm appTerm 25 ref 259 remove 117 remove 62 remove appTerm 260 def appTerm 71 ref appTerm 76 ref appTerm appTerm 25 ref 114 remove 258 ref appTerm 119 remove appTerm 109 remove appTerm 120 remove appTerm appTerm 25 ref 122 remove 237 ref varTerm 261 def appTerm appTerm 125 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 absTerm appTerm absTerm appTerm 262 def absTerm 263 def absTerm 264 def absTerm 265 def absTerm 266 def defineConst 267 def pop 0 ref 1 remove 0 remove 8 remove 106 remove cons opType nil cons cons opType constTerm 268 def 144 remove appTerm 145 ref appTerm 233 remove varTerm 269 def appTerm 146 remove appTerm appTerm 32 remove 33 remove 34 ref 35 remove 34 ref 36 remove 34 ref 37 remove 34 ref 38 remove 34 ref 39 remove 34 ref 40 remove 23 ref 41 remove 23 ref 42 remove 23 ref 43 remove 23 ref 238 remove 34 ref 239 remove 23 ref 46 remove 34 ref 47 remove 23 ref 48 remove 23 ref 240 remove 34 ref 241 remove 23 remove 49 remove 34 remove 50 remove 224 remove 243 remove 67 remove 244 remove 72 remove 245 remove 77 remove 247 remove 249 remove 251 remove 253 remove 87 remove 89 remove 91 remove 93 remove 95 remove 25 ref 254 remove 269 ref appTerm 246 ref appTerm 250 remove appTerm appTerm 25 ref 256 remove 269 remove appTerm 246 remove appTerm 92 remove appTerm appTerm 257 remove 110 remove 25 ref 225 ref 145 remove appTerm 68 remove appTerm 73 remove appTerm appTerm 25 remove 225 remove 260 remove appTerm 71 remove appTerm 76 remove appTerm appTerm 227 remove 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 appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 270 def nil cons cons nil cons nil cons cons 159 ref subst 234 remove nil 160 ref 11 remove 235 ref 14 ref 236 ref 14 ref 237 ref 18 remove 268 remove 258 ref appTerm 242 ref appTerm 255 ref appTerm 261 ref appTerm appTerm 262 remove appTerm 271 def absTerm 272 def appTerm 273 def absTerm 274 def appTerm 275 def absTerm 276 def appTerm nil cons cons nil cons nil cons cons 167 ref subst nil 168 remove 276 remove nil cons cons nil cons nil cons cons 169 remove subst 235 remove nil 160 ref 275 remove nil cons cons nil cons nil cons cons 167 ref subst nil 5 ref 274 remove nil cons cons nil cons nil cons cons 159 ref subst 236 remove nil 160 ref 273 remove nil cons cons nil cons nil cons cons 167 ref subst nil 5 remove 272 remove nil cons cons nil cons nil cons cons 159 remove subst 237 remove nil 160 remove 271 remove nil cons cons nil cons nil cons cons 167 remove subst 267 remove 258 ref refl appThm 266 remove 258 remove appTerm betaConv trans 242 ref refl appThm 265 remove 242 remove appTerm betaConv trans 255 ref refl appThm 264 remove 255 remove appTerm betaConv trans 261 ref refl appThm 263 remove 261 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 14 remove 270 remove appTerm thm