Package hardware-adder-thm: Properties of hardware adder devices
Information
| name | hardware-adder-thm |
| version | 1.15 |
| description | Properties of hardware adder devices |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-06-12 |
| requires | bool hardware-adder-def hardware-bus hardware-thm hardware-wire natural natural-bits |
| show | Data.Bool Hardware Number.Natural |
Files
- Package tarball hardware-adder-thm-1.15.tgz
- Theory source file hardware-adder-thm.thy (included in the package tarball)
Theorems
⊦ Bus.adder2 Bus.nil Bus.nil Bus.nil Bus.nil
⊦ Bus.adder3 Bus.nil Bus.nil Bus.nil Bus.nil Bus.nil
⊦ ∀x y. ∃s c. adder2 x y s c
⊦ ∀x y z. ∃s c. adder3 x y z s c
⊦ ∀x y. Bus.width x = Bus.width y ⇒ ∃s c. Bus.adder2 x y s c
⊦ ∀x y s c. adder2 x y s c ⇒ adder3 x y ground s c
⊦ ∀x y s c.
Bus.adder2 (Bus.single x) (Bus.single y) (Bus.single s)
(Bus.single c) ⇔ adder2 x y s c
⊦ ∀x y s c n. Bus.adder2 x y s c ∧ Bus.width x = n ⇒ Bus.width s = n
⊦ ∀x y s c n. Bus.adder2 x y s c ∧ Bus.width x = n ⇒ Bus.width c = n
⊦ ∀x y z s c n. Bus.adder3 x y z s c ∧ Bus.width x = n ⇒ Bus.width s = n
⊦ ∀x y z s c n. Bus.adder3 x y z s c ∧ Bus.width x = n ⇒ Bus.width c = n
⊦ ∀x y z.
Bus.width x = Bus.width y ∧ Bus.width x = Bus.width z ⇒
∃s c. Bus.adder3 x y z s c
⊦ ∀x y n s c.
Bus.width x = n ∧ Bus.adder2 x y s c ⇒
Bus.adder3 x y (Bus.ground n) s c
⊦ ∀x y z s c.
Bus.adder3 (Bus.single x) (Bus.single y) (Bus.single z) (Bus.single s)
(Bus.single c) ⇔ adder3 x y z s c
⊦ ∀ld xs xc xb.
SumCarry.shiftRight ld xs xc xb ⇒
∃r. Bus.width xs = r + 1 ∧ Bus.width xc = r + 1
⊦ ∀x y s c.
Bus.adder2 x y s c ⇒
∃n.
Bus.width x = n ∧ Bus.width y = n ∧ Bus.width s = n ∧ Bus.width c = n
⊦ ∀w x y z s c n.
Bus.adder4 w x y z s c ∧ Bus.width w = n + 1 ⇒ Bus.width c = n + 1
⊦ ∀w x y z s c n.
Bus.adder4 w x y z s c ∧ Bus.width w = n + 1 ⇒ Bus.width s = n + 2
⊦ ∀x y s c t.
Bus.adder2 x y s c ⇒
Bits.toNatural (Bus.signal x t) + Bits.toNatural (Bus.signal y t) =
Bits.toNatural (Bus.signal s t) + 2 * Bits.toNatural (Bus.signal c t)
⊦ ∀x y s c t.
adder2 x y s c ⇒
fromBool (signal x t) + fromBool (signal y t) =
fromBool (signal s t) + 2 * fromBool (signal c t)
⊦ ∀x1 x2 y1 y2 s1 s2 c1 c2.
Bus.adder2 x1 y1 s1 c1 ∧ Bus.adder2 x2 y2 s2 c2 ⇒
Bus.adder2 (Bus.append x1 x2) (Bus.append y1 y2) (Bus.append s1 s2)
(Bus.append c1 c2)
⊦ ∀x y z s c.
Bus.adder3 x y z s c ⇒
∃n.
Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n ∧
Bus.width s = n ∧ Bus.width c = n
⊦ ∀w x y z.
¬(Bus.width w = 0) ∧ Bus.width w = Bus.width x ∧
Bus.width w = Bus.width y ∧ Bus.width w = Bus.width z ⇒
∃s c. Bus.adder4 w x y z s c
⊦ ∀xh xt yh yt sh st ch ct.
Bus.adder2 (Bus.append (Bus.single xh) xt)
(Bus.append (Bus.single yh) yt) (Bus.append (Bus.single sh) st)
(Bus.append (Bus.single ch) ct) ⇔
adder2 xh yh sh ch ∧ Bus.adder2 xt yt st ct
⊦ ∀x y z s c t.
Bus.adder3 x y z s c ⇒
Bits.toNatural (Bus.signal x t) +
(Bits.toNatural (Bus.signal y t) + Bits.toNatural (Bus.signal z t)) =
Bits.toNatural (Bus.signal s t) + 2 * Bits.toNatural (Bus.signal c t)
⊦ ∀x y z s c t.
adder3 x y z s c ⇒
fromBool (signal x t) +
(fromBool (signal y t) + fromBool (signal z t)) =
fromBool (signal s t) + 2 * fromBool (signal c t)
⊦ ∀x y s c i xi yi si ci.
Bus.adder2 x y s c ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧
Bus.wire s i si ∧ Bus.wire c i ci ⇒ adder2 xi yi si ci
⊦ ∀x1 x2 y1 y2 z1 z2 s1 s2 c1 c2.
Bus.adder3 x1 y1 z1 s1 c1 ∧ Bus.adder3 x2 y2 z2 s2 c2 ⇒
Bus.adder3 (Bus.append x1 x2) (Bus.append y1 y2) (Bus.append z1 z2)
(Bus.append s1 s2) (Bus.append c1 c2)
⊦ ∀x y s c k n xs ys ss cs.
Bus.adder2 x y s c ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub s k n ss ∧ Bus.sub c k n cs ⇒ Bus.adder2 xs ys ss cs
⊦ ∀xh xt yh yt zh zt sh st ch ct.
Bus.adder3 (Bus.append (Bus.single xh) xt)
(Bus.append (Bus.single yh) yt) (Bus.append (Bus.single zh) zt)
(Bus.append (Bus.single sh) st) (Bus.append (Bus.single ch) ct) ⇔
adder3 xh yh zh sh ch ∧ Bus.adder3 xt yt zt st ct
⊦ ∀w x y z s c t.
Bus.adder4 w x y z s c ⇒
Bits.toNatural (Bus.signal w t) +
(Bits.toNatural (Bus.signal x t) +
(Bits.toNatural (Bus.signal y t) + Bits.toNatural (Bus.signal z t))) =
Bits.toNatural (Bus.signal s t) + 2 * Bits.toNatural (Bus.signal c t)
⊦ ∀x y z s c i xi yi zi si ci.
Bus.adder3 x y z s c ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧
Bus.wire z i zi ∧ Bus.wire s i si ∧ Bus.wire c i ci ⇒
adder3 xi yi zi si ci
⊦ ∀x ld xs xc xb t k.
(∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
Bits.toNatural (Bus.signal xs t) +
2 * Bits.toNatural (Bus.signal xc t) = x ∧
SumCarry.shiftRight ld xs xc xb ⇒ (signal xb (t + k) ⇔ Bits.bit x k)
⊦ ∀x y z s c k n xs ys zs ss cs.
Bus.adder3 x y z s c ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub z k n zs ∧ Bus.sub s k n ss ∧ Bus.sub c k n cs ⇒
Bus.adder3 xs ys zs ss cs
⊦ ∀w x y z s c.
Bus.adder4 w x y z s c ⇒
∃n.
Bus.width w = n + 1 ∧ Bus.width x = n + 1 ∧ Bus.width y = n + 1 ∧
Bus.width z = n + 1 ∧ Bus.width s = n + 2 ∧ Bus.width c = n + 1
External Type Operators
- →
- bool
- Data
- List
- Data.List.list
- List
- Hardware
- bus
- wire
- Number
- Natural
- natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- Data.List.::
- Data.List.[]
- Bool
- Hardware
- adder2
- adder3
- and2
- case1
- connect
- ground
- majority3
- signal
- xor2
- xor3
- Bus
- Bus.adder2
- Bus.adder3
- Bus.adder4
- Bus.and2
- Bus.append
- Bus.case1
- Bus.delay
- Bus.ground
- Bus.majority3
- Bus.nil
- Bus.signal
- Bus.single
- Bus.sub
- Bus.width
- Bus.wire
- Bus.xor2
- Bus.xor3
- SumCarry
- SumCarry.shiftRight
- Number
- Natural
- *
- +
- <
- ≤
- bit0
- bit1
- fromBool
- suc
- zero
- Bits
- Bits.bit
- Bits.cons
- Bits.head
- Bits.shiftLeft
- Bits.shiftRight
- Bits.tail
- Bits.toNatural
- Natural
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ bit0 0 = 0
⊦ Bits.toNatural Data.List.[] = 0
⊦ Bus.and2 Bus.nil Bus.nil Bus.nil
⊦ Bus.xor2 Bus.nil Bus.nil Bus.nil
⊦ ∀t. t ⇒ t
⊦ ∀n. 0 ≤ n
⊦ ∀n. n ≤ n
⊦ ⊥ ⇔ ∀p. p
⊦ Bus.majority3 Bus.nil Bus.nil Bus.nil Bus.nil
⊦ Bus.xor3 Bus.nil Bus.nil Bus.nil Bus.nil
⊦ ∀t. ¬signal ground t
⊦ ∀n. n ≤ suc n
⊦ (¬) = λp. p ⇒ ⊥
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀x. ∃y. connect x y
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. (⊤ ⇔ t) ⇔ t
⊦ ∀t. (t ⇔ ⊤) ⇔ t
⊦ ∀t. ⊥ ∧ t ⇔ ⊥
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ∧ ⊥ ⇔ ⊥
⊦ ∀t. t ∧ ⊤ ⇔ t
⊦ ∀t. ⊥ ⇒ t ⇔ ⊤
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀t. ⊥ ∨ t ⇔ t
⊦ ∀t. ⊤ ∨ t ⇔ ⊤
⊦ ∀t. t ∨ t ⇔ t
⊦ ∀n. ¬(suc n = 0)
⊦ ∀m. m * 0 = 0
⊦ ∀n. 0 + n = n
⊦ ∀m. m + 0 = m
⊦ ∀k. Bits.shiftLeft 0 k = 0
⊦ ∀n. Bits.shiftRight n 0 = n
⊦ ∀t. Bus.signal Bus.nil t = Data.List.[]
⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t
⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t
⊦ ∀w. Bus.width (Bus.single w) = 1
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ ∀t. fromBool (signal ground t) = 0
⊦ ∀m. m * 1 = m
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀b. Bits.toNatural (Data.List.:: b Data.List.[]) = fromBool b
⊦ ∀x y. ∃z. and2 x y z
⊦ ∀x y. ∃z. xor2 x y z
⊦ ∀m. suc m = m + 1
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀h t. Bits.head (Bits.cons h t) ⇔ h
⊦ ∀h t. Bits.tail (Bits.cons h t) = t
⊦ ∀b. fromBool b = if b then 1 else 0
⊦ ∀x. Bus.width x = 0 ⇔ x = Bus.nil
⊦ ∀n. 0 < n ⇔ ¬(n = 0)
⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀x y. x = y ⇒ y = x
⊦ ∀m n. m + n = n + m
⊦ ∀n t. Bits.toNatural (Bus.signal (Bus.ground n) t) = 0
⊦ ∀w x y. ∃z. majority3 w x y z
⊦ ∀w x y. ∃z. xor3 w x y z
⊦ ∀n i. Bits.bit n i ⇔ Bits.head (Bits.shiftRight n i)
⊦ ∀m. m = 0 ∨ ∃n. m = suc n
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀h t. Bits.toNatural (Data.List.:: h t) = Bits.cons h (Bits.toNatural t)
⊦ ∀m n. m + suc n = suc (m + n)
⊦ ∀n k. Bits.shiftRight n (suc k) = Bits.tail (Bits.shiftRight n k)
⊦ ∀m n. suc m + n = suc (m + n)
⊦ ∀m n. m < m + n ⇔ 0 < n
⊦ ∀m n. suc m = suc n ⇔ m = n
⊦ ∀x y. Bus.width (Bus.append x y) = Bus.width x + Bus.width y
⊦ ∀x y. Bus.sub x 0 (Bus.width x) y ⇔ y = x
⊦ ∀w t.
Bus.signal (Bus.single w) t = Data.List.:: (signal w t) Data.List.[]
⊦ ∀x i. i < Bus.width x ⇒ ∃w. Bus.wire x i w
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀x y. Bus.width x = Bus.width y ⇒ ∃z. Bus.and2 x y z
⊦ ∀x y. Bus.width x = Bus.width y ⇒ ∃z. Bus.xor2 x y z
⊦ ∀x y z. and2 x y z ⇒ majority3 x y ground z
⊦ ∀x y z. xor2 x y z ⇒ xor3 x y ground z
⊦ ∀h t. Bits.cons h t = fromBool h + 2 * t
⊦ ∀p q. (∀x. p x ⇒ q) ⇔ (∃x. p x) ⇒ q
⊦ ∀x y z. x = y ∧ y = z ⇒ x = z
⊦ ∀p q r. p ⇒ q ⇒ r ⇔ p ∧ q ⇒ r
⊦ ∀t1 t2 t3. (t1 ∧ t2) ∧ t3 ⇔ t1 ∧ t2 ∧ t3
⊦ ∀w x v. Bus.wire (Bus.append (Bus.single w) x) 0 v ⇔ v = w
⊦ ∀x y t. connect x y ⇒ (signal y t ⇔ signal x t)
⊦ ∀m n p. m + (n + p) = m + n + p
⊦ ∀m n p. m + n = m + p ⇔ n = p
⊦ ∀p m n. m + p = n + p ⇔ m = n
⊦ ∀k n1 n2. Bits.shiftLeft n1 k = Bits.shiftLeft n2 k ⇔ n1 = n2
⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀x k n y. Bus.sub x k n y ⇒ Bus.width y = n
⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0
⊦ ∀x y z. Bus.sub (Bus.append x y) 0 (Bus.width x) z ⇔ z = x
⊦ ∀x i w. Bus.wire x i w ⇔ Bus.sub x i 1 (Bus.single w)
⊦ ∀x y z.
Bus.and2 (Bus.single x) (Bus.single y) (Bus.single z) ⇔ and2 x y z
⊦ ∀x y z.
Bus.xor2 (Bus.single x) (Bus.single y) (Bus.single z) ⇔ xor2 x y z
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ ∀x y z. Bus.sub (Bus.append x y) (Bus.width x) (Bus.width y) z ⇔ z = y
⊦ ∀w i v. Bus.wire (Bus.single w) i v ⇔ i = 0 ∧ v = w
⊦ ∀m n p. m * (n + p) = m * n + m * p
⊦ ∀x k n. k + n ≤ Bus.width x ⇒ ∃y. Bus.sub x k n y
⊦ ∀x y t. Bus.delay x y ⇒ Bus.signal y (t + 1) = Bus.signal x t
⊦ ∀w x t.
Bus.signal (Bus.append (Bus.single w) x) t =
Data.List.:: (signal w t) (Bus.signal x t)
⊦ ∀w x i v.
Bus.wire (Bus.append (Bus.single w) x) (suc i) v ⇔ Bus.wire x i v
⊦ ∀x y i w. Bus.wire (Bus.append x y) (Bus.width x + i) w ⇔ Bus.wire y i w
⊦ ∀x y s c. Bus.adder2 x y s c ⇔ Bus.xor2 x y s ∧ Bus.and2 x y c
⊦ ∀x y s c. adder2 x y s c ⇔ xor2 x y s ∧ and2 x y c
⊦ ∀w x y z.
Bus.majority3 (Bus.single w) (Bus.single x) (Bus.single y)
(Bus.single z) ⇔ majority3 w x y z
⊦ ∀w x y z.
Bus.xor3 (Bus.single w) (Bus.single x) (Bus.single y) (Bus.single z) ⇔
xor3 w x y z
⊦ ∀x y n z.
Bus.width x = n ∧ Bus.and2 x y z ⇒ Bus.majority3 x y (Bus.ground n) z
⊦ ∀x y n z.
Bus.width x = n ∧ Bus.xor2 x y z ⇒ Bus.xor3 x y (Bus.ground n) z
⊦ ∀w x y.
Bus.width w = Bus.width x ∧ Bus.width w = Bus.width y ⇒
∃z. Bus.majority3 w x y z
⊦ ∀w x y.
Bus.width w = Bus.width x ∧ Bus.width w = Bus.width y ⇒
∃z. Bus.xor3 w x y z
⊦ ∀n x.
Bus.width x = suc n ⇔
∃w y. x = Bus.append (Bus.single w) y ∧ Bus.width y = n
⊦ ∀x y k n z.
Bus.sub (Bus.append x y) (Bus.width x + k) n z ⇔ Bus.sub y k n z
⊦ ∀x y t.
Bits.toNatural (Bus.signal (Bus.append x y) t) =
Bits.toNatural (Bus.signal x t) +
Bits.shiftLeft (Bits.toNatural (Bus.signal y t)) (Bus.width x)
⊦ ∀x y z.
Bus.and2 x y z ⇒
∃n. Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n
⊦ ∀x y z.
Bus.xor2 x y z ⇒
∃n. Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n
⊦ ∀x y z s c.
Bus.adder3 x y z s c ⇔ Bus.xor3 x y z s ∧ Bus.majority3 x y z c
⊦ ∀x y z s c. adder3 x y z s c ⇔ xor3 x y z s ∧ majority3 x y z c
⊦ ∀s x y z t.
Bus.case1 s x y z ⇒
Bus.signal z t = if signal s t then Bus.signal x t else Bus.signal y t
⊦ ∀s x y z t.
case1 s x y z ⇒
(signal z t ⇔ if signal s t then signal x t else signal y t)
⊦ ∀w x y z t.
xor3 w x y z ⇒ (signal z t ⇔ signal w t ⇔ signal x t ⇔ signal y t)
⊦ ∀x1 x2 y1 y2 z1 z2.
Bus.and2 x1 y1 z1 ∧ Bus.and2 x2 y2 z2 ⇒
Bus.and2 (Bus.append x1 x2) (Bus.append y1 y2) (Bus.append z1 z2)
⊦ ∀x1 x2 y1 y2 z1 z2.
Bus.xor2 x1 y1 z1 ∧ Bus.xor2 x2 y2 z2 ⇒
Bus.xor2 (Bus.append x1 x2) (Bus.append y1 y2) (Bus.append z1 z2)
⊦ ∀x y z k m n.
Bus.sub x k m y ∧ Bus.sub x (k + m) n z ⇒
Bus.sub x k (m + n) (Bus.append y z)
⊦ ∀w x y z.
Bus.majority3 w x y z ⇒
∃n.
Bus.width w = n ∧ Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n
⊦ ∀w x y z.
Bus.xor3 w x y z ⇒
∃n.
Bus.width w = n ∧ Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n
⊦ ∀w1 w2 x1 x2 y1 y2 z1 z2.
Bus.majority3 w1 x1 y1 z1 ∧ Bus.majority3 w2 x2 y2 z2 ⇒
Bus.majority3 (Bus.append w1 w2) (Bus.append x1 x2) (Bus.append y1 y2)
(Bus.append z1 z2)
⊦ ∀w1 w2 x1 x2 y1 y2 z1 z2.
Bus.xor3 w1 x1 y1 z1 ∧ Bus.xor3 w2 x2 y2 z2 ⇒
Bus.xor3 (Bus.append w1 w2) (Bus.append x1 x2) (Bus.append y1 y2)
(Bus.append z1 z2)
⊦ ∀x y z k n xs ys zs.
Bus.and2 x y z ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub z k n zs ⇒ Bus.and2 xs ys zs
⊦ ∀x y z k n xs ys zs.
Bus.xor2 x y z ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub z k n zs ⇒ Bus.xor2 xs ys zs
⊦ ∀w x y z t.
majority3 w x y z ⇒
(signal z t ⇔
signal w t ∧ signal x t ∨ signal w t ∧ signal y t ∨
signal x t ∧ signal y t)
⊦ ∀w x y z k n ws xs ys zs.
Bus.majority3 w x y z ∧ Bus.sub w k n ws ∧ Bus.sub x k n xs ∧
Bus.sub y k n ys ∧ Bus.sub z k n zs ⇒ Bus.majority3 ws xs ys zs
⊦ ∀w x y z k n ws xs ys zs.
Bus.xor3 w x y z ∧ Bus.sub w k n ws ∧ Bus.sub x k n xs ∧
Bus.sub y k n ys ∧ Bus.sub z k n zs ⇒ Bus.xor3 ws xs ys zs
⊦ ∀ld xs xc xb.
SumCarry.shiftRight ld xs xc xb ⇔
∃r sp sq sr cp cq cr xs0 xs1 sq0 sq1 sq2 sq3 cp0 cp1 cq0 cq1.
Bus.width xs = r + 1 ∧ Bus.width xc = r + 1 ∧ Bus.width sp = r ∧
Bus.width sq = r + 1 ∧ Bus.width sr = r ∧ Bus.width cp = r + 1 ∧
Bus.width cq = r + 1 ∧ Bus.width cr = r + 1 ∧ Bus.wire xs 0 xs0 ∧
Bus.sub xs 1 r xs1 ∧ Bus.wire sq 0 sq0 ∧ Bus.sub sq 0 r sq1 ∧
Bus.sub sq 1 r sq2 ∧ Bus.wire sq r sq3 ∧ Bus.sub cp 0 r cp0 ∧
Bus.wire cp r cp1 ∧ Bus.sub cq 0 r cq0 ∧ Bus.wire cq r cq1 ∧
Bus.adder2 sp cp0 sq1 cq0 ∧ connect cp1 sq3 ∧ connect ground cq1 ∧
case1 ld xs0 sq0 xb ∧ Bus.case1 ld xs1 sq2 sr ∧
Bus.case1 ld xc cq cr ∧ Bus.delay sr sp ∧ Bus.delay cr cp
⊦ ∀w x y z s c.
Bus.adder4 w x y z s c ⇔
∃n p q z0 z1 s0 s1 s2 c0 c1 p0 p1 q1 q2.
Bus.width w = n + 1 ∧ Bus.width x = n + 1 ∧ Bus.width y = n + 1 ∧
Bus.width z = n + 1 ∧ Bus.width s = n + 2 ∧ Bus.width c = n + 1 ∧
Bus.width p = n + 1 ∧ Bus.width q = n + 1 ∧ Bus.wire z 0 z0 ∧
Bus.sub z 1 n z1 ∧ Bus.wire s 0 s0 ∧ Bus.sub s 1 n s1 ∧
Bus.wire s (n + 1) s2 ∧ Bus.wire c 0 c0 ∧ Bus.sub c 1 n c1 ∧
Bus.wire p 0 p0 ∧ Bus.sub p 1 n p1 ∧ Bus.sub q 0 n q1 ∧
Bus.wire q n q2 ∧ Bus.adder3 w x y p q ∧ adder2 p0 z0 s0 c0 ∧
Bus.adder3 p1 q1 z1 s1 c1 ∧ connect q2 s2