path: "vendor/opentheory/data/theories/hardware-wire-def/hardware-wire-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 "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 "=" const 11 def 0 ref 2 ref 0 ref 2 ref 3 ref cons opType 12 def nil cons cons opType 13 def constTerm 14 def "Hardware.connect" "_33607" 1 ref var 15 def "_33608" 1 ref var 16 def 7 ref 0 ref 0 ref "Number.Natural.natural" typeOp nil opType 17 def 3 ref cons opType 18 def 3 ref cons opType constTerm 19 def "t" 17 ref var 20 def 14 ref "Hardware.signal" const 0 ref 1 ref 18 remove nil cons cons opType constTerm 21 def 16 ref varTerm 22 def appTerm 20 ref varTerm 23 def appTerm appTerm 21 ref 15 ref varTerm 24 def appTerm 23 ref appTerm appTerm absTerm appTerm 25 def absTerm 26 def absTerm 27 def defineConst 28 def pop 0 ref 1 ref 4 remove nil cons cons opType 29 def constTerm 30 def 6 ref varTerm 31 def appTerm 10 ref varTerm 32 def appTerm appTerm 19 ref 20 ref 14 ref 21 ref 32 ref appTerm 33 def 23 ref appTerm 34 def appTerm 35 def 21 ref 31 ref appTerm 23 ref appTerm 36 def appTerm absTerm appTerm appTerm absTerm appTerm absTerm 37 def nil cons cons nil cons nil cons cons "A" 1 ref nil cons cons nil cons nil nil cons cons 14 ref 7 remove 0 ref 0 ref "A" varType 38 def 3 ref cons opType 39 def 3 ref cons opType 40 def constTerm 41 def "P" 39 ref var varTerm 42 def appTerm appTerm refl "p" 39 ref var 43 def 11 ref 0 ref 39 remove 40 ref nil cons cons opType constTerm 43 remove varTerm appTerm "x" 38 remove var "Data.Bool.T" const 2 ref constTerm 44 def absTerm appTerm absTerm 45 def 42 ref appTerm betaConv appThm nil 11 remove 0 ref 40 ref 0 ref 40 remove 3 remove cons opType nil cons cons opType constTerm 41 remove appTerm 45 remove appTerm axiom 42 remove refl appThm eqMp sym subst 46 def subst 15 remove nil "t" 2 ref var 47 def 9 ref 16 ref 14 ref 30 ref 24 ref appTerm 22 ref appTerm appTerm 25 remove appTerm 48 def absTerm 49 def appTerm nil cons cons nil cons nil cons cons 14 ref 47 ref varTerm 50 def appTerm 44 ref appTerm assume sym nil 44 remove axiom 51 def eqMp 50 remove assume 51 remove deductAntisym deductAntisym 52 def subst nil 5 ref 49 remove nil cons cons nil cons nil cons cons 46 ref subst 16 remove nil 47 ref 48 remove nil cons cons nil cons nil cons cons 52 ref subst 28 remove 24 ref refl appThm 27 remove 24 remove appTerm betaConv trans 22 ref refl appThm 26 remove 22 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 37 remove appTerm thm nil 5 ref 6 ref 9 ref 10 ref 14 ref "Hardware.not" "_33631" 1 ref var 53 def "_33632" 1 ref var 54 def 19 ref 20 ref 14 ref 21 ref 54 ref varTerm 55 def appTerm 23 ref appTerm appTerm "Data.Bool.~" const 12 remove constTerm 56 def 21 ref 53 ref varTerm 57 def appTerm 23 ref appTerm appTerm appTerm absTerm appTerm 58 def absTerm 59 def absTerm 60 def defineConst 61 def pop 29 ref constTerm 62 def 31 ref appTerm 32 ref appTerm appTerm 19 ref 20 ref 35 remove 56 ref 36 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm 63 def nil cons cons nil cons nil cons cons 46 ref subst 53 remove nil 47 ref 9 ref 54 ref 14 ref 62 ref 57 ref appTerm 55 ref appTerm appTerm 58 remove appTerm 64 def absTerm 65 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 65 remove nil cons cons nil cons nil cons cons 46 ref subst 54 remove nil 47 ref 64 remove nil cons cons nil cons nil cons cons 52 ref subst 61 remove 57 ref refl appThm 60 remove 57 remove appTerm betaConv trans 55 ref refl appThm 59 remove 55 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 63 remove appTerm thm nil 5 ref 6 ref 9 ref 10 ref 14 ref "Hardware.delay" "_33619" 1 ref var 66 def "_33620" 1 ref var 67 def 19 ref 20 ref 14 ref 21 ref 67 ref varTerm 68 def appTerm "Number.Natural.+" const 0 ref 17 ref 0 ref 17 ref 17 ref nil cons cons opType 69 def nil cons cons opType constTerm 23 ref appTerm "Number.Natural.bit1" const 69 remove constTerm "Number.Natural.zero" const 17 remove constTerm appTerm appTerm 70 def appTerm appTerm 21 ref 66 ref varTerm 71 def appTerm 23 ref appTerm appTerm absTerm appTerm 72 def absTerm 73 def absTerm 74 def defineConst 75 def pop 29 ref constTerm 76 def 31 ref appTerm 77 def 32 ref appTerm appTerm 19 ref 20 ref 14 ref 33 remove 70 remove appTerm appTerm 36 ref appTerm absTerm appTerm appTerm absTerm appTerm absTerm 78 def nil cons cons nil cons nil cons cons 46 ref subst 66 remove nil 47 ref 9 ref 67 ref 14 ref 76 ref 71 ref appTerm 68 ref appTerm appTerm 72 remove appTerm 79 def absTerm 80 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 80 remove nil cons cons nil cons nil cons cons 46 ref subst 67 remove nil 47 ref 79 remove nil cons cons nil cons nil cons cons 52 ref subst 75 remove 71 ref refl appThm 74 remove 71 remove appTerm betaConv trans 68 ref refl appThm 73 remove 68 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 78 remove appTerm thm nil 5 ref 6 ref 9 ref 10 ref 9 ref "z" 1 ref var 81 def 14 ref "Hardware.nor2" "_33750" 1 ref var 82 def "_33751" 1 ref var 83 def "_33752" 1 ref var 84 def "Data.Bool.?" const 8 remove constTerm 85 def "zn" 1 ref var 86 def "Data.Bool./\\" const 13 ref constTerm 87 def "Hardware.or2" "_33664" 1 ref var 88 def "_33665" 1 ref var 89 def "_33666" 1 ref var 90 def 19 ref 20 ref 14 ref 21 ref 90 ref varTerm 91 def appTerm 23 ref appTerm appTerm "Data.Bool.\\/" const 13 ref constTerm 92 def 21 ref 88 ref varTerm 93 def appTerm 23 ref appTerm appTerm 21 ref 89 ref varTerm 94 def appTerm 23 ref appTerm appTerm appTerm absTerm appTerm 95 def absTerm 96 def absTerm 97 def absTerm 98 def defineConst 99 def pop 0 ref 1 ref 29 ref nil cons cons opType 100 def constTerm 101 def 82 ref varTerm 102 def appTerm 83 ref varTerm 103 def appTerm 86 ref varTerm 104 def appTerm appTerm 62 ref 104 ref appTerm 105 def 84 ref varTerm 106 def appTerm appTerm absTerm appTerm 107 def absTerm 108 def absTerm 109 def absTerm 110 def defineConst 111 def pop 100 ref constTerm 112 def 31 ref appTerm 32 ref appTerm 81 ref varTerm 113 def appTerm appTerm 85 ref 86 remove 87 ref 101 ref 31 ref appTerm 32 ref appTerm 114 def 104 remove appTerm appTerm 105 remove 113 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 115 def nil cons cons nil cons nil cons cons 46 ref subst 82 remove nil 47 ref 9 ref 83 ref 9 ref 84 ref 14 ref 112 remove 102 ref appTerm 103 ref appTerm 106 ref appTerm appTerm 107 remove appTerm 116 def absTerm 117 def appTerm 118 def absTerm 119 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 119 remove nil cons cons nil cons nil cons cons 46 ref subst 83 remove nil 47 ref 118 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 117 remove nil cons cons nil cons nil cons cons 46 ref subst 84 remove nil 47 ref 116 remove nil cons cons nil cons nil cons cons 52 ref subst 111 remove 102 ref refl appThm 110 remove 102 remove appTerm betaConv trans 103 ref refl appThm 109 remove 103 remove appTerm betaConv trans 106 ref refl appThm 108 remove 106 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 115 remove appTerm thm nil 5 ref 6 ref 9 ref 10 ref 9 ref 81 ref 14 ref "Hardware.and2" "_33643" 1 ref var 120 def "_33644" 1 ref var 121 def "_33645" 1 ref var 122 def 19 ref 20 ref 14 ref 21 ref 122 ref varTerm 123 def appTerm 23 ref appTerm appTerm 87 ref 21 ref 120 ref varTerm 124 def appTerm 23 ref appTerm appTerm 21 ref 121 ref varTerm 125 def appTerm 23 ref appTerm appTerm appTerm absTerm appTerm 126 def absTerm 127 def absTerm 128 def absTerm 129 def defineConst 130 def pop 100 ref constTerm 131 def 31 ref appTerm 132 def 32 ref appTerm 133 def 113 ref appTerm appTerm 19 ref 20 ref 14 ref 21 ref 113 ref appTerm 23 ref appTerm appTerm 134 def 87 ref 36 ref appTerm 34 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 135 def nil cons cons nil cons nil cons cons 46 ref subst 120 remove nil 47 ref 9 ref 121 ref 9 ref 122 ref 14 ref 131 ref 124 ref appTerm 125 ref appTerm 123 ref appTerm appTerm 126 remove appTerm 136 def absTerm 137 def appTerm 138 def absTerm 139 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 139 remove nil cons cons nil cons nil cons cons 46 ref subst 121 remove nil 47 ref 138 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 137 remove nil cons cons nil cons nil cons cons 46 ref subst 122 remove nil 47 ref 136 remove nil cons cons nil cons nil cons cons 52 ref subst 130 remove 124 ref refl appThm 129 remove 124 remove appTerm betaConv trans 125 ref refl appThm 128 remove 125 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 9 ref 135 remove appTerm thm nil 5 ref 6 ref 9 ref 10 ref 9 ref 81 ref 14 ref 114 remove 113 ref appTerm appTerm 19 ref 20 ref 134 ref 92 remove 36 ref appTerm 34 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 140 def nil cons cons nil cons nil cons cons 46 ref subst 88 remove nil 47 ref 9 ref 89 ref 9 ref 90 ref 14 ref 101 ref 93 ref appTerm 94 ref appTerm 91 ref appTerm appTerm 95 remove appTerm 141 def absTerm 142 def appTerm 143 def absTerm 144 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 144 remove nil cons cons nil cons nil cons cons 46 ref subst 89 remove nil 47 ref 143 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 142 remove nil cons cons nil cons nil cons cons 46 ref subst 90 remove nil 47 ref 141 remove nil cons cons nil cons nil cons cons 52 ref subst 99 remove 93 ref refl appThm 98 remove 93 remove appTerm betaConv trans 94 ref refl appThm 97 remove 94 remove appTerm betaConv trans 91 ref refl appThm 96 remove 91 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 140 remove appTerm thm nil 5 ref 6 ref 9 ref 10 ref 14 ref "Hardware.pulse" "_33738" 1 ref var 145 def "_33739" 1 ref var 146 def 85 ref "xd" 1 ref var 147 def 85 ref "xn" 1 ref var 148 def 87 ref 76 ref 145 ref varTerm 149 def appTerm 147 ref varTerm 150 def appTerm appTerm 87 ref 62 remove 150 ref appTerm 148 ref varTerm 151 def appTerm appTerm 152 def 131 ref 149 ref appTerm 151 ref appTerm 146 ref varTerm 153 def appTerm appTerm appTerm absTerm appTerm absTerm appTerm 154 def absTerm 155 def absTerm 156 def defineConst 157 def pop 29 remove constTerm 158 def 31 ref appTerm 32 ref appTerm appTerm 85 ref 147 remove 85 ref 148 remove 87 ref 77 remove 150 remove appTerm appTerm 152 remove 132 remove 151 remove appTerm 32 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm 159 def nil cons cons nil cons nil cons cons 46 ref subst 145 remove nil 47 ref 9 ref 146 ref 14 ref 158 remove 149 ref appTerm 153 ref appTerm appTerm 154 remove appTerm 160 def absTerm 161 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 161 remove nil cons cons nil cons nil cons cons 46 ref subst 146 remove nil 47 ref 160 remove nil cons cons nil cons nil cons cons 52 ref subst 157 remove 149 ref refl appThm 156 remove 149 remove appTerm betaConv trans 153 ref refl appThm 155 remove 153 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 159 remove appTerm thm nil 5 ref "w" 1 ref var 162 def 9 ref 6 ref 9 ref 10 ref 9 ref 81 ref 14 ref "Hardware.and3" "_33771" 1 ref var 163 def "_33772" 1 ref var 164 def "_33773" 1 ref var 165 def "_33774" 1 ref var 166 def 85 ref "wx" 1 ref var 167 def 87 ref 131 ref 163 ref varTerm 168 def appTerm 164 ref varTerm 169 def appTerm 167 ref varTerm 170 def appTerm appTerm 131 ref 170 ref appTerm 171 def 165 ref varTerm 172 def appTerm 166 ref varTerm 173 def appTerm appTerm absTerm appTerm 174 def absTerm 175 def absTerm 176 def absTerm 177 def absTerm 178 def defineConst 179 def pop 0 ref 1 ref 100 ref nil cons cons opType 180 def constTerm 181 def 162 ref varTerm 182 def appTerm 31 ref appTerm 32 ref appTerm 113 ref appTerm appTerm 85 ref 167 ref 87 ref 131 ref 182 ref appTerm 183 def 31 ref appTerm 170 ref appTerm appTerm 184 def 171 remove 32 ref appTerm 113 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 185 def nil cons cons nil cons nil cons cons 46 ref subst 163 remove nil 47 ref 9 ref 164 ref 9 ref 165 ref 9 ref 166 ref 14 ref 181 remove 168 ref appTerm 169 ref appTerm 172 ref appTerm 173 ref appTerm appTerm 174 remove appTerm 186 def absTerm 187 def appTerm 188 def absTerm 189 def appTerm 190 def absTerm 191 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 191 remove nil cons cons nil cons nil cons cons 46 ref subst 164 remove nil 47 ref 190 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 189 remove nil cons cons nil cons nil cons cons 46 ref subst 165 remove nil 47 ref 188 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 187 remove nil cons cons nil cons nil cons cons 46 ref subst 166 remove nil 47 ref 186 remove nil cons cons nil cons nil cons cons 52 ref subst 179 remove 168 ref refl appThm 178 remove 168 remove appTerm betaConv trans 169 ref refl appThm 177 remove 169 remove appTerm betaConv trans 172 ref refl appThm 176 remove 172 remove appTerm betaConv trans 173 ref refl appThm 175 remove 173 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 185 remove appTerm thm nil 5 ref 162 ref 9 ref 6 ref 9 ref 10 ref 9 ref 81 ref 14 ref "Hardware.or3" "_33803" 1 ref var 192 def "_33804" 1 ref var 193 def "_33805" 1 ref var 194 def "_33806" 1 ref var 195 def 85 ref 167 ref 87 ref 101 ref 192 ref varTerm 196 def appTerm 193 ref varTerm 197 def appTerm 170 ref appTerm appTerm 101 ref 170 ref appTerm 198 def 194 ref varTerm 199 def appTerm 195 ref varTerm 200 def appTerm appTerm absTerm appTerm 201 def absTerm 202 def absTerm 203 def absTerm 204 def absTerm 205 def defineConst 206 def pop 180 ref constTerm 207 def 182 ref appTerm 31 ref appTerm 32 ref appTerm 113 ref appTerm appTerm 85 ref 167 ref 87 ref 101 ref 182 ref appTerm 208 def 31 ref appTerm 170 ref appTerm appTerm 198 remove 32 ref appTerm 113 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 209 def nil cons cons nil cons nil cons cons 46 ref subst 192 remove nil 47 ref 9 ref 193 ref 9 ref 194 ref 9 ref 195 ref 14 ref 207 ref 196 ref appTerm 197 ref appTerm 199 ref appTerm 200 ref appTerm appTerm 201 remove appTerm 210 def absTerm 211 def appTerm 212 def absTerm 213 def appTerm 214 def absTerm 215 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 215 remove nil cons cons nil cons nil cons cons 46 ref subst 193 remove nil 47 ref 214 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 213 remove nil cons cons nil cons nil cons cons 46 ref subst 194 remove nil 47 ref 212 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 211 remove nil cons cons nil cons nil cons cons 46 ref subst 195 remove nil 47 ref 210 remove nil cons cons nil cons nil cons cons 52 ref subst 206 remove 196 ref refl appThm 205 remove 196 remove appTerm betaConv trans 197 ref refl appThm 204 remove 197 remove appTerm betaConv trans 199 ref refl appThm 203 remove 199 remove appTerm betaConv trans 200 ref refl appThm 202 remove 200 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 209 remove appTerm thm nil 5 ref 162 ref 9 ref 6 ref 9 ref 10 ref 9 ref 81 ref 14 ref "Hardware.xor3" "_33835" 1 ref var 216 def "_33836" 1 ref var 217 def "_33837" 1 ref var 218 def "_33838" 1 ref var 219 def 85 ref 167 ref 87 ref "Hardware.xor2" "_33685" 1 ref var 220 def "_33686" 1 ref var 221 def "_33687" 1 ref var 222 def 19 ref 20 ref 14 ref 21 ref 222 ref varTerm 223 def appTerm 23 ref appTerm appTerm 56 ref 14 ref 21 ref 220 ref varTerm 224 def appTerm 23 ref appTerm appTerm 21 ref 221 ref varTerm 225 def appTerm 23 ref appTerm appTerm appTerm appTerm absTerm appTerm 226 def absTerm 227 def absTerm 228 def absTerm 229 def defineConst 230 def pop 100 ref constTerm 231 def 216 ref varTerm 232 def appTerm 217 ref varTerm 233 def appTerm 170 ref appTerm appTerm 231 ref 170 ref appTerm 234 def 218 ref varTerm 235 def appTerm 219 ref varTerm 236 def appTerm appTerm absTerm appTerm 237 def absTerm 238 def absTerm 239 def absTerm 240 def absTerm 241 def defineConst 242 def pop 180 ref constTerm 243 def 182 ref appTerm 31 ref appTerm 32 ref appTerm 113 ref appTerm appTerm 85 ref 167 ref 87 ref 231 ref 182 ref appTerm 31 ref appTerm 170 ref appTerm appTerm 234 remove 32 ref appTerm 113 ref appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 244 def nil cons cons nil cons nil cons cons 46 ref subst 216 remove nil 47 ref 9 ref 217 ref 9 ref 218 ref 9 ref 219 ref 14 ref 243 remove 232 ref appTerm 233 ref appTerm 235 ref appTerm 236 ref appTerm appTerm 237 remove appTerm 245 def absTerm 246 def appTerm 247 def absTerm 248 def appTerm 249 def absTerm 250 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 250 remove nil cons cons nil cons nil cons cons 46 ref subst 217 remove nil 47 ref 249 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 248 remove nil cons cons nil cons nil cons cons 46 ref subst 218 remove nil 47 ref 247 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 246 remove nil cons cons nil cons nil cons cons 46 ref subst 219 remove nil 47 ref 245 remove nil cons cons nil cons nil cons cons 52 ref subst 242 remove 232 ref refl appThm 241 remove 232 remove appTerm betaConv trans 233 ref refl appThm 240 remove 233 remove appTerm betaConv trans 235 ref refl appThm 239 remove 235 remove appTerm betaConv trans 236 ref refl appThm 238 remove 236 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 244 remove appTerm thm nil 5 ref 6 ref 9 ref 10 ref 9 ref 81 ref 14 ref 231 ref 31 ref appTerm 32 ref appTerm 113 ref appTerm appTerm 19 ref 20 ref 134 ref 56 remove 14 ref 36 ref appTerm 34 ref appTerm appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 251 def nil cons cons nil cons nil cons cons 46 ref subst 220 remove nil 47 ref 9 ref 221 ref 9 ref 222 ref 14 ref 231 remove 224 ref appTerm 225 ref appTerm 223 ref appTerm appTerm 226 remove appTerm 252 def absTerm 253 def appTerm 254 def absTerm 255 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 255 remove nil cons cons nil cons nil cons cons 46 ref subst 221 remove nil 47 ref 254 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 253 remove nil cons cons nil cons nil cons cons 46 ref subst 222 remove nil 47 ref 252 remove nil cons cons nil cons nil cons cons 52 ref subst 230 remove 224 ref refl appThm 229 remove 224 remove appTerm betaConv trans 225 ref refl appThm 228 remove 225 remove appTerm betaConv trans 223 ref refl appThm 227 remove 223 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 251 remove appTerm thm nil 5 ref "s" 1 ref var 256 def 9 ref 6 ref 9 ref 10 ref 9 ref 81 ref 14 ref "Hardware.case1" "_33706" 1 ref var 257 def "_33707" 1 ref var 258 def "_33708" 1 ref var 259 def "_33709" 1 ref var 260 def 19 ref 20 ref 14 ref 21 ref 260 ref varTerm 261 def appTerm 23 ref appTerm appTerm "Data.Bool.cond" const 0 remove 2 remove 13 remove nil cons cons opType constTerm 262 def 21 ref 257 ref varTerm 263 def appTerm 23 ref appTerm appTerm 21 ref 258 ref varTerm 264 def appTerm 23 ref appTerm appTerm 21 ref 259 ref varTerm 265 def appTerm 23 ref appTerm appTerm appTerm absTerm appTerm 266 def absTerm 267 def absTerm 268 def absTerm 269 def absTerm 270 def defineConst 271 def pop 180 ref constTerm 272 def 256 remove varTerm 273 def appTerm 31 ref appTerm 32 ref appTerm 113 ref appTerm appTerm 19 remove 20 remove 134 remove 262 remove 21 remove 273 remove appTerm 23 remove appTerm appTerm 36 remove appTerm 34 remove appTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 274 def nil cons cons nil cons nil cons cons 46 ref subst 257 remove nil 47 ref 9 ref 258 ref 9 ref 259 ref 9 ref 260 ref 14 ref 272 ref 263 ref appTerm 264 ref appTerm 265 ref appTerm 261 ref appTerm appTerm 266 remove appTerm 275 def absTerm 276 def appTerm 277 def absTerm 278 def appTerm 279 def absTerm 280 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 280 remove nil cons cons nil cons nil cons cons 46 ref subst 258 remove nil 47 ref 279 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 278 remove nil cons cons nil cons nil cons cons 46 ref subst 259 remove nil 47 ref 277 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 276 remove nil cons cons nil cons nil cons cons 46 ref subst 260 remove nil 47 ref 275 remove nil cons cons nil cons nil cons cons 52 ref subst 271 remove 263 ref refl appThm 270 remove 263 remove appTerm betaConv trans 264 ref refl appThm 269 remove 264 remove appTerm betaConv trans 265 ref refl appThm 268 remove 265 remove appTerm betaConv trans 261 ref refl appThm 267 remove 261 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 274 remove appTerm thm nil 5 ref "ld" 1 ref var 281 def 9 ref 162 ref 9 ref 6 ref 14 ref "Hardware.sticky" "_33899" 1 ref var 282 def "_33900" 1 ref var 283 def "_33901" 1 ref var 284 def 85 ref "p" 1 ref var 285 def 85 ref "q" 1 ref var 286 def 85 ref "r" 1 ref var 287 def 87 ref 272 ref 282 ref varTerm 288 def appTerm "Hardware.ground" const 1 ref constTerm 289 def appTerm 285 ref varTerm 290 def appTerm 286 ref varTerm 291 def appTerm appTerm 87 ref 101 remove 283 ref varTerm 292 def appTerm 291 ref appTerm 287 ref varTerm 293 def appTerm appTerm 87 ref 76 remove 293 ref appTerm 290 ref appTerm appTerm 294 def 30 remove 293 ref appTerm 295 def 284 ref varTerm 296 def appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 297 def absTerm 298 def absTerm 299 def absTerm 300 def defineConst 301 def pop 100 remove constTerm 302 def 281 remove varTerm 303 def appTerm 182 ref appTerm 31 ref appTerm appTerm 85 ref 285 remove 85 ref 286 remove 85 ref 287 remove 87 ref 272 remove 303 remove appTerm 289 remove appTerm 290 remove appTerm 291 ref appTerm appTerm 87 ref 208 remove 291 remove appTerm 293 remove appTerm appTerm 294 remove 295 remove 31 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 304 def nil cons cons nil cons nil cons cons 46 ref subst 282 remove nil 47 ref 9 ref 283 ref 9 ref 284 ref 14 ref 302 remove 288 ref appTerm 292 ref appTerm 296 ref appTerm appTerm 297 remove appTerm 305 def absTerm 306 def appTerm 307 def absTerm 308 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 308 remove nil cons cons nil cons nil cons cons 46 ref subst 283 remove nil 47 ref 307 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 306 remove nil cons cons nil cons nil cons cons 46 ref subst 284 remove nil 47 ref 305 remove nil cons cons nil cons nil cons cons 52 ref subst 301 remove 288 ref refl appThm 300 remove 288 remove appTerm betaConv trans 292 ref refl appThm 299 remove 292 remove appTerm betaConv trans 296 ref refl appThm 298 remove 296 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 ref 304 remove appTerm thm nil 5 ref 162 remove 9 ref 6 remove 9 ref 10 remove 9 ref 81 remove 14 ref "Hardware.majority3" "_33867" 1 ref var 309 def "_33868" 1 ref var 310 def "_33869" 1 ref var 311 def "_33870" 1 ref var 312 def 85 ref 167 ref 85 ref "wy" 1 ref var 313 def 85 ref "xy" 1 remove var 314 def 87 ref 131 ref 309 ref varTerm 315 def appTerm 316 def 310 ref varTerm 317 def appTerm 170 ref appTerm appTerm 87 ref 316 remove 311 ref varTerm 318 def appTerm 313 ref varTerm 319 def appTerm appTerm 87 ref 131 remove 317 ref appTerm 318 ref appTerm 314 ref varTerm 320 def appTerm appTerm 207 remove 170 remove appTerm 319 ref appTerm 320 ref appTerm 321 def 312 ref varTerm 322 def appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 323 def absTerm 324 def absTerm 325 def absTerm 326 def absTerm 327 def defineConst 328 def pop 180 remove constTerm 329 def 182 remove appTerm 31 remove appTerm 32 ref appTerm 113 ref appTerm appTerm 85 ref 167 remove 85 ref 313 remove 85 remove 314 remove 184 remove 87 ref 183 remove 32 remove appTerm 319 remove appTerm appTerm 87 remove 133 remove 320 remove appTerm appTerm 321 remove 113 remove appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 330 def nil cons cons nil cons nil cons cons 46 ref subst 309 remove nil 47 ref 9 ref 310 ref 9 ref 311 ref 9 ref 312 ref 14 remove 329 remove 315 ref appTerm 317 ref appTerm 318 ref appTerm 322 ref appTerm appTerm 323 remove appTerm 331 def absTerm 332 def appTerm 333 def absTerm 334 def appTerm 335 def absTerm 336 def appTerm nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 336 remove nil cons cons nil cons nil cons cons 46 ref subst 310 remove nil 47 ref 335 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 ref 334 remove nil cons cons nil cons nil cons cons 46 ref subst 311 remove nil 47 ref 333 remove nil cons cons nil cons nil cons cons 52 ref subst nil 5 remove 332 remove nil cons cons nil cons nil cons cons 46 remove subst 312 remove nil 47 remove 331 remove nil cons cons nil cons nil cons cons 52 remove subst 328 remove 315 ref refl appThm 327 remove 315 remove appTerm betaConv trans 317 ref refl appThm 326 remove 317 remove appTerm betaConv trans 318 ref refl appThm 325 remove 318 remove appTerm betaConv trans 322 ref refl appThm 324 remove 322 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 9 remove 330 remove appTerm thm