path: "vendor/opentheory/data/theories/hardware-bus-def/hardware-bus-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 0 ref "Number.Natural.natural" typeOp nil opType 8 def 3 ref cons opType 9 def 3 ref cons opType 10 def constTerm 11 def "i" 8 ref var 12 def 7 ref 0 ref 0 ref "Hardware.wire" typeOp nil opType 13 def 3 ref cons opType 14 def 3 ref cons opType constTerm 15 def "w" 13 ref var 16 def "=" const 17 def 0 ref 2 ref 0 ref 2 ref 3 ref cons opType nil cons cons opType 18 def constTerm 19 def "Hardware.Bus.wire" "_34072" 1 ref var 20 def "_34073" 8 ref var 21 def "_34074" 13 ref var 22 def "Hardware.Bus.sub" const 0 ref 1 ref 0 ref 8 ref 0 ref 8 ref 4 ref nil cons 23 def cons opType nil cons cons opType nil cons cons opType constTerm 24 def 20 ref varTerm 25 def appTerm 21 ref varTerm 26 def appTerm "Number.Natural.bit1" const 0 ref 8 ref 8 ref nil cons 27 def cons opType 28 def constTerm "Number.Natural.zero" const 8 ref constTerm appTerm 29 def appTerm "Hardware.Bus.single" const 0 ref 13 ref 1 ref nil cons 30 def cons opType constTerm 31 def 22 ref varTerm 32 def appTerm appTerm 33 def absTerm 34 def absTerm 35 def absTerm 36 def defineConst 37 def pop 0 ref 1 ref 0 ref 8 ref 14 ref nil cons 38 def cons opType nil cons cons opType constTerm 39 def 6 ref varTerm 40 def appTerm 12 ref varTerm 41 def appTerm 42 def 16 remove varTerm 43 def appTerm appTerm 24 remove 40 ref appTerm 41 ref appTerm 29 ref appTerm 31 remove 43 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 44 def nil cons cons nil cons nil cons cons "A" 30 remove cons nil cons nil nil cons 45 def cons 19 ref 7 ref 0 ref 0 ref "A" varType 46 def 3 ref cons opType 47 def 3 ref cons opType 48 def constTerm 49 def "P" 47 ref var varTerm 50 def appTerm appTerm refl "p" 47 ref var 51 def 17 ref 0 ref 47 remove 48 ref nil cons cons opType constTerm 51 remove varTerm appTerm "x" 46 remove var "Data.Bool.T" const 2 ref constTerm 52 def absTerm appTerm absTerm 53 def 50 ref appTerm betaConv appThm nil 17 ref 0 ref 48 ref 0 ref 48 remove 3 ref cons opType nil cons cons opType constTerm 49 remove appTerm 53 remove appTerm axiom 50 remove refl appThm eqMp sym 54 def subst 55 def subst 20 remove nil "t" 2 remove var 56 def 11 ref 21 ref 15 ref 22 ref 19 ref 39 ref 25 ref appTerm 26 ref appTerm 32 ref appTerm appTerm 33 remove appTerm 57 def absTerm 58 def appTerm 59 def absTerm 60 def appTerm nil cons cons nil cons nil cons cons 19 ref 56 ref varTerm 61 def appTerm 52 ref appTerm assume sym nil 52 remove axiom 62 def eqMp 61 remove assume 62 remove deductAntisym deductAntisym 63 def subst nil "P" 9 ref var 60 remove nil cons cons nil cons nil cons cons "A" 27 ref cons nil cons 45 ref cons 54 ref subst subst 21 remove nil 56 ref 59 remove nil cons cons nil cons nil cons cons 63 ref subst nil "P" 14 remove var 64 def 58 remove nil cons cons nil cons nil cons cons "A" 13 ref nil cons cons nil cons 45 ref cons 54 ref subst 65 def subst 22 remove nil 56 ref 57 remove nil cons cons nil cons nil cons cons 63 ref subst 37 remove 25 ref refl appThm 36 remove 25 remove appTerm betaConv trans 26 ref refl appThm 35 remove 26 remove appTerm betaConv trans 32 ref refl appThm 34 remove 32 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 7 ref 0 ref 4 remove 3 ref cons opType 66 def constTerm 67 def 44 remove appTerm thm nil 5 ref 6 ref 67 ref "y" 1 ref var 68 def 19 ref "Hardware.Bus.reverse" "_34093" 1 ref var 69 def "_34094" 1 ref var 70 def "Data.Bool./\\" const 18 ref constTerm 71 def 17 ref 0 ref 8 ref 9 remove nil cons cons opType constTerm 72 def "Hardware.Bus.width" const 0 ref 1 ref 27 remove cons opType constTerm 73 def 69 ref varTerm 74 def appTerm 75 def appTerm 73 ref 70 ref varTerm 76 def appTerm appTerm appTerm 11 ref 12 ref 11 ref "j" 8 ref var 77 def 15 ref "xi" 13 ref var 78 def 15 ref "yj" 13 ref var 79 def "Data.Bool.==>" const 18 remove constTerm 80 def 71 ref 72 ref "Number.Natural.+" const 0 ref 8 ref 28 remove nil cons cons opType constTerm 81 def 41 ref appTerm 81 remove 77 ref varTerm 82 def appTerm 29 remove appTerm appTerm appTerm 83 def 75 remove appTerm appTerm 71 ref 39 ref 74 ref appTerm 41 ref appTerm 78 ref varTerm 84 def appTerm appTerm 39 ref 76 ref appTerm 82 ref appTerm 79 ref varTerm 85 def appTerm appTerm appTerm appTerm 17 ref 0 ref 13 ref 38 remove cons opType 86 def constTerm 84 ref appTerm 85 ref appTerm 87 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm 88 def absTerm 89 def absTerm 90 def defineConst 91 def pop 0 ref 1 ref 23 remove cons opType 92 def constTerm 93 def 40 ref appTerm 68 ref varTerm 94 def appTerm appTerm 71 ref 72 ref 73 ref 40 ref appTerm 95 def appTerm 96 def 73 ref 94 ref appTerm 97 def appTerm appTerm 11 ref 12 ref 11 ref 77 remove 15 ref 78 ref 15 ref 79 remove 80 ref 71 ref 83 remove 95 remove appTerm appTerm 71 ref 42 remove 84 ref appTerm appTerm 98 def 39 ref 94 ref appTerm 99 def 82 remove appTerm 85 remove appTerm appTerm appTerm appTerm 87 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm appTerm absTerm appTerm absTerm 100 def nil cons cons nil cons nil cons cons 55 ref subst 69 remove nil 56 ref 67 ref 70 ref 19 ref 93 remove 74 ref appTerm 76 ref appTerm appTerm 88 remove appTerm 101 def absTerm 102 def appTerm nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 102 remove nil cons cons nil cons nil cons cons 55 ref subst 70 remove nil 56 ref 101 remove nil cons cons nil cons nil cons cons 63 ref subst 91 remove 74 ref refl appThm 90 remove 74 remove appTerm betaConv trans 76 ref refl appThm 89 remove 76 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 67 ref 100 remove appTerm thm nil "P" 0 ref 86 ref 3 ref cons opType 103 def var "r" 86 ref var 104 def 67 ref 6 ref 67 ref 68 ref 19 ref "Hardware.Bus.lift2" "_34105" 86 ref var 105 def "_34106" 1 ref var 106 def "_34107" 1 ref var 107 def "Data.Bool.?" const 108 def 10 remove constTerm 109 def "n" 8 remove var 110 def 71 ref 72 ref 73 ref 106 ref varTerm 111 def appTerm appTerm 110 ref varTerm 112 def appTerm appTerm 71 ref 72 ref 73 ref 107 ref varTerm 113 def appTerm appTerm 112 ref appTerm appTerm 11 ref 12 ref 15 ref 78 ref 15 ref "yi" 13 ref var 114 def 80 ref 71 ref 39 ref 111 ref appTerm 41 ref appTerm 84 ref appTerm appTerm 39 ref 113 ref appTerm 41 ref appTerm 114 ref varTerm 115 def appTerm appTerm appTerm 105 ref varTerm 116 def 84 ref appTerm 115 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm appTerm absTerm appTerm 117 def absTerm 118 def absTerm 119 def absTerm 120 def defineConst 121 def pop 0 ref 86 ref 92 ref nil cons 122 def cons opType constTerm 123 def 104 remove varTerm 124 def appTerm 40 ref appTerm 94 ref appTerm appTerm 109 ref 110 ref 71 ref 96 remove 112 ref appTerm appTerm 125 def 71 ref 72 ref 97 remove appTerm 112 ref appTerm appTerm 126 def 11 ref 12 ref 15 ref 78 ref 15 ref 114 ref 80 ref 98 ref 99 remove 41 ref appTerm 115 ref appTerm 127 def appTerm appTerm 124 remove 84 ref appTerm 115 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 128 def nil cons cons nil cons nil cons cons "A" 86 ref nil cons 129 def cons nil cons 45 ref cons 54 ref subst subst 105 remove nil 56 ref 67 ref 106 ref 67 ref 107 ref 19 ref 123 ref 116 ref appTerm 111 ref appTerm 113 ref appTerm appTerm 117 remove appTerm 130 def absTerm 131 def appTerm 132 def absTerm 133 def appTerm nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 133 remove nil cons cons nil cons nil cons cons 55 ref subst 106 remove nil 56 ref 132 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 131 remove nil cons cons nil cons nil cons cons 55 ref subst 107 remove nil 56 ref 130 remove nil cons cons nil cons nil cons cons 63 ref subst 121 remove 116 ref refl appThm 120 remove 116 remove appTerm betaConv trans 111 ref refl appThm 119 remove 111 remove appTerm betaConv trans 113 ref refl appThm 118 remove 113 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 7 ref 0 ref 103 remove 3 ref cons opType constTerm 128 remove appTerm thm nil "P" 0 ref 0 ref 13 ref 129 remove cons opType 134 def 3 ref cons opType 135 def var "r" 134 ref var 136 def 67 ref 6 ref 67 ref 68 ref 67 ref "z" 1 ref var 137 def 19 ref "Hardware.Bus.lift3" "_34126" 134 ref var 138 def "_34127" 1 ref var 139 def "_34128" 1 ref var 140 def "_34129" 1 ref var 141 def 109 ref 110 ref 71 ref 72 ref 73 ref 139 ref varTerm 142 def appTerm appTerm 112 ref appTerm appTerm 71 ref 72 ref 73 ref 140 ref varTerm 143 def appTerm appTerm 112 ref appTerm appTerm 71 ref 72 ref 73 ref 141 ref varTerm 144 def appTerm appTerm 112 ref appTerm appTerm 11 ref 12 ref 15 ref 78 ref 15 ref 114 ref 15 ref "zi" 13 ref var 145 def 80 ref 71 ref 39 ref 142 ref appTerm 41 ref appTerm 84 ref appTerm appTerm 71 ref 39 ref 143 ref appTerm 41 ref appTerm 115 ref appTerm appTerm 39 ref 144 ref appTerm 41 ref appTerm 145 ref varTerm 146 def appTerm appTerm appTerm appTerm 138 ref varTerm 147 def 84 ref appTerm 115 ref appTerm 146 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm appTerm appTerm absTerm appTerm 148 def absTerm 149 def absTerm 150 def absTerm 151 def absTerm 152 def defineConst 153 def pop 0 ref 134 ref 0 ref 1 ref 122 remove cons opType 154 def nil cons 155 def cons opType constTerm 156 def 136 remove varTerm 157 def appTerm 40 ref appTerm 94 ref appTerm 137 ref varTerm 158 def appTerm appTerm 109 remove 110 remove 125 remove 126 remove 71 ref 72 remove 73 remove 158 ref appTerm appTerm 112 remove appTerm appTerm 11 remove 12 remove 15 ref 78 remove 15 ref 114 remove 15 ref 145 remove 80 remove 98 remove 71 ref 127 remove appTerm 39 remove 158 ref appTerm 41 remove appTerm 146 ref appTerm appTerm appTerm appTerm 157 remove 84 remove appTerm 115 remove appTerm 146 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 159 def nil cons cons nil cons nil cons cons "A" 134 ref nil cons 160 def cons nil cons 45 remove cons 54 remove subst subst 138 remove nil 56 ref 67 ref 139 ref 67 ref 140 ref 67 ref 141 ref 19 ref 156 ref 147 ref appTerm 142 ref appTerm 143 ref appTerm 144 ref appTerm appTerm 148 remove appTerm 161 def absTerm 162 def appTerm 163 def absTerm 164 def appTerm 165 def absTerm 166 def appTerm nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 166 remove nil cons cons nil cons nil cons cons 55 ref subst 139 remove nil 56 ref 165 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 164 remove nil cons cons nil cons nil cons cons 55 ref subst 140 remove nil 56 ref 163 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 162 remove nil cons cons nil cons nil cons cons 55 ref subst 141 remove nil 56 ref 161 remove nil cons cons nil cons nil cons cons 63 ref subst 153 remove 147 ref refl appThm 152 remove 147 remove appTerm betaConv trans 142 ref refl appThm 151 remove 142 remove appTerm betaConv trans 143 ref refl appThm 150 remove 143 remove appTerm betaConv trans 144 ref refl appThm 149 remove 144 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 7 remove 0 ref 135 remove 3 ref cons opType constTerm 159 remove appTerm thm "Hardware.Bus.connect" 123 ref "Hardware.connect" const 86 ref constTerm appTerm 167 def defineConst 168 def pop 169 def pop 168 remove nil 17 ref 0 ref 92 ref 0 ref 92 ref 3 ref cons opType nil cons cons opType constTerm 170 def 169 remove 92 ref constTerm appTerm 167 remove appTerm thm "Hardware.Bus.delay" 123 ref "Hardware.delay" const 86 ref constTerm appTerm 171 def defineConst 172 def pop 173 def pop 172 remove nil 170 ref 173 remove 92 ref constTerm appTerm 171 remove appTerm thm "Hardware.Bus.not" 123 remove "Hardware.not" const 86 remove constTerm appTerm 174 def defineConst 175 def pop 176 def pop 175 remove nil 170 remove 176 remove 92 remove constTerm appTerm 174 remove appTerm thm "Hardware.Bus.and2" 156 ref "Hardware.and2" const 134 ref constTerm appTerm 177 def defineConst 178 def pop 179 def pop 178 remove nil 17 remove 0 ref 154 ref 0 ref 154 ref 3 remove cons opType nil cons cons opType constTerm 180 def 179 remove 154 ref constTerm 181 def appTerm 177 remove appTerm thm "Hardware.Bus.or2" 156 ref "Hardware.or2" const 134 ref constTerm appTerm 182 def defineConst 183 def pop 184 def pop 183 remove nil 180 ref 184 remove 154 ref constTerm 185 def appTerm 182 remove appTerm thm "Hardware.Bus.xor2" 156 ref "Hardware.xor2" const 134 remove constTerm appTerm 186 def defineConst 187 def pop 188 def pop 187 remove nil 180 ref 188 remove 154 remove constTerm 189 def appTerm 186 remove appTerm thm nil 64 remove "s" 13 ref var 190 def 180 ref "Hardware.Bus.case1" "_34158" 13 ref var 191 def 156 ref "Hardware.case1" const 0 ref 13 ref 160 remove cons opType constTerm 192 def 191 ref varTerm 193 def appTerm appTerm 194 def absTerm 195 def defineConst 196 def pop 0 ref 13 remove 155 ref cons opType constTerm 197 def 190 remove varTerm 198 def appTerm appTerm 156 remove 192 remove 198 remove appTerm appTerm appTerm absTerm 199 def nil cons cons nil cons nil cons cons 65 remove subst 191 remove nil 56 ref 180 remove 197 remove 193 ref appTerm appTerm 194 remove appTerm nil cons cons nil cons nil cons cons 63 ref subst 196 remove 193 ref refl appThm 195 remove 193 remove appTerm betaConv trans eqMp absThm eqMp nil 15 remove 199 remove appTerm thm nil 5 ref "w" 1 ref var 200 def 67 ref 6 ref 67 ref 68 ref 67 ref 137 ref 19 ref "Hardware.Bus.and3" "_34163" 1 ref var 201 def "_34164" 1 ref var 202 def "_34165" 1 ref var 203 def "_34166" 1 ref var 204 def 108 remove 66 remove constTerm 205 def "wx" 1 ref var 206 def 71 ref 181 ref 201 ref varTerm 207 def appTerm 202 ref varTerm 208 def appTerm 206 ref varTerm 209 def appTerm appTerm 181 ref 209 ref appTerm 210 def 203 ref varTerm 211 def appTerm 204 ref varTerm 212 def appTerm appTerm absTerm appTerm 213 def absTerm 214 def absTerm 215 def absTerm 216 def absTerm 217 def defineConst 218 def pop 0 remove 1 ref 155 remove cons opType 219 def constTerm 220 def 200 ref varTerm 221 def appTerm 40 ref appTerm 94 ref appTerm 158 ref appTerm appTerm 205 ref 206 ref 71 ref 181 ref 221 ref appTerm 222 def 40 ref appTerm 209 ref appTerm appTerm 223 def 210 remove 94 ref appTerm 158 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 224 def nil cons cons nil cons nil cons cons 55 ref subst 201 remove nil 56 ref 67 ref 202 ref 67 ref 203 ref 67 ref 204 ref 19 ref 220 remove 207 ref appTerm 208 ref appTerm 211 ref appTerm 212 ref appTerm appTerm 213 remove appTerm 225 def absTerm 226 def appTerm 227 def absTerm 228 def appTerm 229 def absTerm 230 def appTerm nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 230 remove nil cons cons nil cons nil cons cons 55 ref subst 202 remove nil 56 ref 229 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 228 remove nil cons cons nil cons nil cons cons 55 ref subst 203 remove nil 56 ref 227 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 226 remove nil cons cons nil cons nil cons cons 55 ref subst 204 remove nil 56 ref 225 remove nil cons cons nil cons nil cons cons 63 ref subst 218 remove 207 ref refl appThm 217 remove 207 remove appTerm betaConv trans 208 ref refl appThm 216 remove 208 remove appTerm betaConv trans 211 ref refl appThm 215 remove 211 remove appTerm betaConv trans 212 ref refl appThm 214 remove 212 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 67 ref 224 remove appTerm thm nil 5 ref 200 ref 67 ref 6 ref 67 ref 68 ref 67 ref 137 ref 19 ref "Hardware.Bus.or3" "_34195" 1 ref var 231 def "_34196" 1 ref var 232 def "_34197" 1 ref var 233 def "_34198" 1 ref var 234 def 205 ref 206 ref 71 ref 185 ref 231 ref varTerm 235 def appTerm 232 ref varTerm 236 def appTerm 209 ref appTerm appTerm 185 ref 209 ref appTerm 237 def 233 ref varTerm 238 def appTerm 234 ref varTerm 239 def appTerm appTerm absTerm appTerm 240 def absTerm 241 def absTerm 242 def absTerm 243 def absTerm 244 def defineConst 245 def pop 219 ref constTerm 246 def 221 ref appTerm 40 ref appTerm 94 ref appTerm 158 ref appTerm appTerm 205 ref 206 ref 71 ref 185 remove 221 ref appTerm 40 ref appTerm 209 ref appTerm appTerm 237 remove 94 ref appTerm 158 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 247 def nil cons cons nil cons nil cons cons 55 ref subst 231 remove nil 56 ref 67 ref 232 ref 67 ref 233 ref 67 ref 234 ref 19 ref 246 ref 235 ref appTerm 236 ref appTerm 238 ref appTerm 239 ref appTerm appTerm 240 remove appTerm 248 def absTerm 249 def appTerm 250 def absTerm 251 def appTerm 252 def absTerm 253 def appTerm nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 253 remove nil cons cons nil cons nil cons cons 55 ref subst 232 remove nil 56 ref 252 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 251 remove nil cons cons nil cons nil cons cons 55 ref subst 233 remove nil 56 ref 250 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 249 remove nil cons cons nil cons nil cons cons 55 ref subst 234 remove nil 56 ref 248 remove nil cons cons nil cons nil cons cons 63 ref subst 245 remove 235 ref refl appThm 244 remove 235 remove appTerm betaConv trans 236 ref refl appThm 243 remove 236 remove appTerm betaConv trans 238 ref refl appThm 242 remove 238 remove appTerm betaConv trans 239 ref refl appThm 241 remove 239 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 67 ref 247 remove appTerm thm nil 5 ref 200 ref 67 ref 6 ref 67 ref 68 ref 67 ref 137 ref 19 ref "Hardware.Bus.xor3" "_34227" 1 ref var 254 def "_34228" 1 ref var 255 def "_34229" 1 ref var 256 def "_34230" 1 ref var 257 def 205 ref 206 ref 71 ref 189 ref 254 ref varTerm 258 def appTerm 255 ref varTerm 259 def appTerm 209 ref appTerm appTerm 189 ref 209 ref appTerm 260 def 256 ref varTerm 261 def appTerm 257 ref varTerm 262 def appTerm appTerm absTerm appTerm 263 def absTerm 264 def absTerm 265 def absTerm 266 def absTerm 267 def defineConst 268 def pop 219 ref constTerm 269 def 221 ref appTerm 40 ref appTerm 94 ref appTerm 158 ref appTerm appTerm 205 ref 206 ref 71 ref 189 remove 221 ref appTerm 40 ref appTerm 209 ref appTerm appTerm 260 remove 94 ref appTerm 158 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 270 def nil cons cons nil cons nil cons cons 55 ref subst 254 remove nil 56 ref 67 ref 255 ref 67 ref 256 ref 67 ref 257 ref 19 ref 269 remove 258 ref appTerm 259 ref appTerm 261 ref appTerm 262 ref appTerm appTerm 263 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 63 ref subst nil 5 ref 276 remove nil cons cons nil cons nil cons cons 55 ref subst 255 remove nil 56 ref 275 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 274 remove nil cons cons nil cons nil cons cons 55 ref subst 256 remove nil 56 ref 273 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 272 remove nil cons cons nil cons nil cons cons 55 ref subst 257 remove nil 56 ref 271 remove nil cons cons nil cons nil cons cons 63 ref subst 268 remove 258 ref refl appThm 267 remove 258 remove appTerm betaConv trans 259 ref refl appThm 266 remove 259 remove appTerm betaConv trans 261 ref refl appThm 265 remove 261 remove appTerm betaConv trans 262 ref refl appThm 264 remove 262 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 67 ref 270 remove appTerm thm nil 5 ref 200 remove 67 ref 6 remove 67 ref 68 remove 67 ref 137 remove 19 ref "Hardware.Bus.majority3" "_34259" 1 ref var 277 def "_34260" 1 ref var 278 def "_34261" 1 ref var 279 def "_34262" 1 ref var 280 def 205 ref 206 ref 205 ref "wy" 1 ref var 281 def 205 ref "xy" 1 remove var 282 def 71 ref 181 ref 277 ref varTerm 283 def appTerm 284 def 278 ref varTerm 285 def appTerm 209 ref appTerm appTerm 71 ref 284 remove 279 ref varTerm 286 def appTerm 281 ref varTerm 287 def appTerm appTerm 71 ref 181 ref 285 ref appTerm 286 ref appTerm 282 ref varTerm 288 def appTerm appTerm 246 remove 209 remove appTerm 287 ref appTerm 288 ref appTerm 289 def 280 ref varTerm 290 def appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 291 def absTerm 292 def absTerm 293 def absTerm 294 def absTerm 295 def defineConst 296 def pop 219 remove constTerm 297 def 221 remove appTerm 40 ref appTerm 94 ref appTerm 158 ref appTerm appTerm 205 ref 206 remove 205 ref 281 remove 205 remove 282 remove 223 remove 71 ref 222 remove 94 ref appTerm 287 remove appTerm appTerm 71 remove 181 remove 40 remove appTerm 94 remove appTerm 288 remove appTerm appTerm 289 remove 158 remove appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 298 def nil cons cons nil cons nil cons cons 55 ref subst 277 remove nil 56 ref 67 ref 278 ref 67 ref 279 ref 67 ref 280 ref 19 remove 297 remove 283 ref appTerm 285 ref appTerm 286 ref appTerm 290 ref appTerm appTerm 291 remove appTerm 299 def absTerm 300 def appTerm 301 def absTerm 302 def appTerm 303 def absTerm 304 def appTerm nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 304 remove nil cons cons nil cons nil cons cons 55 ref subst 278 remove nil 56 ref 303 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 ref 302 remove nil cons cons nil cons nil cons cons 55 ref subst 279 remove nil 56 ref 301 remove nil cons cons nil cons nil cons cons 63 ref subst nil 5 remove 300 remove nil cons cons nil cons nil cons cons 55 remove subst 280 remove nil 56 remove 299 remove nil cons cons nil cons nil cons cons 63 remove subst 296 remove 283 ref refl appThm 295 remove 283 remove appTerm betaConv trans 285 ref refl appThm 294 remove 285 remove appTerm betaConv trans 286 ref refl appThm 293 remove 286 remove appTerm betaConv trans 290 ref refl appThm 292 remove 290 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 67 remove 298 remove appTerm thm