Package hardware-adder-thm: Properties of hardware adder devices

Information

name	hardware-adder-thm
version	1.18
description	Properties of hardware adder devices
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2014-11-01
checksum	13f877448595c9ffe62091926ae96deb9b4c5571
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.18.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)

⊦ ∀x₁ x₂ y₁ y₂ s₁ s₂ c₁ c₂.
    Bus.adder2 x₁ y₁ s₁ c₁ ∧ Bus.adder2 x₂ y₂ s₂ c₂ ⇒
    Bus.adder2 (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append s₁ s₂)
      (Bus.append c₁ c₂)

⊦ ∀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

⊦ ∀x₁ x₂ y₁ y₂ z₁ z₂ s₁ s₂ c₁ c₂.
    Bus.adder3 x₁ y₁ z₁ s₁ c₁ ∧ Bus.adder3 x₂ y₂ z₂ s₂ c₂ ⇒
    Bus.adder3 (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append z₁ z₂)
      (Bus.append s₁ s₂) (Bus.append c₁ c₂)

⊦ ∀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
Hardware
- bus
- wire
Number
- Natural
  - natural

External Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - Data.List.::
  - Data.List.[]
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

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

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀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

⊦ ∀t₁ t₂ t₃. (t₁ ∧ t₂) ∧ t₃ ⇔ t₁ ∧ t₂ ∧ t₃

⊦ ∀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 n₁ n₂. Bits.shiftLeft n₁ k = Bits.shiftLeft n₂ k ⇔ n₁ = n₂

⊦ ∀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)

⊦ ∀x₁ x₂ y₁ y₂ z₁ z₂.
Bus.and2 x₁ y₁ z₁ ∧ Bus.and2 x₂ y₂ z₂ ⇒
Bus.and2 (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append z₁ z₂)

⊦ ∀x₁ x₂ y₁ y₂ z₁ z₂.
Bus.xor2 x₁ y₁ z₁ ∧ Bus.xor2 x₂ y₂ z₂ ⇒
Bus.xor2 (Bus.append x₁ x₂) (Bus.append y₁ y₂) (Bus.append z₁ z₂)

⊦ ∀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

⊦ ∀w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂.
    Bus.majority3 w₁ x₁ y₁ z₁ ∧ Bus.majority3 w₂ x₂ y₂ z₂ ⇒
    Bus.majority3 (Bus.append w₁ w₂) (Bus.append x₁ x₂) (Bus.append y₁ y₂)
      (Bus.append z₁ z₂)

⊦ ∀w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂.
    Bus.xor3 w₁ x₁ y₁ z₁ ∧ Bus.xor3 w₂ x₂ y₂ z₂ ⇒
    Bus.xor3 (Bus.append w₁ w₂) (Bus.append x₁ x₂) (Bus.append y₁ y₂)
      (Bus.append z₁ z₂)

⊦ ∀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 xs₀ xs₁ sq₀ sq₁ sq₂ sq₃ cp₀ cp₁ cq₀ cq₁.
      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 xs₀ ∧
      Bus.sub xs 1 r xs₁ ∧ Bus.wire sq 0 sq₀ ∧ Bus.sub sq 0 r sq₁ ∧
      Bus.sub sq 1 r sq₂ ∧ Bus.wire sq r sq₃ ∧ Bus.sub cp 0 r cp₀ ∧
      Bus.wire cp r cp₁ ∧ Bus.sub cq 0 r cq₀ ∧ Bus.wire cq r cq₁ ∧
      Bus.adder2 sp cp₀ sq₁ cq₀ ∧ connect cp₁ sq₃ ∧ connect ground cq₁ ∧
      case1 ld xs₀ sq₀ xb ∧ Bus.case1 ld xs₁ sq₂ 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 z₀ z₁ s₀ s₁ s₂ c₀ c₁ p₀ p₁ q₁ q₂.
      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 z₀ ∧
      Bus.sub z 1 n z₁ ∧ Bus.wire s 0 s₀ ∧ Bus.sub s 1 n s₁ ∧
      Bus.wire s (n + 1) s₂ ∧ Bus.wire c 0 c₀ ∧ Bus.sub c 1 n c₁ ∧
      Bus.wire p 0 p₀ ∧ Bus.sub p 1 n p₁ ∧ Bus.sub q 0 n q₁ ∧
      Bus.wire q n q₂ ∧ Bus.adder3 w x y p q ∧ adder2 p₀ z₀ s₀ c₀ ∧
      Bus.adder3 p₁ q₁ z₁ s₁ c₁ ∧ connect q₂ s₂