Package hardware-counter: Hardware counter devices

Information

name	hardware-counter
version	1.15
description	Hardware counter devices
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
requires	bool function hardware-adder hardware-bus hardware-def hardware-thm hardware-wire list natural natural-bits pair set stream
show	Data.Bool Data.List Data.Pair Data.Stream Function Hardware Number.Natural Set

Files

Package tarball hardware-counter-1.15.tgz
Theory source file hardware-counter.thy (included in the package tarball)

Defined Constants

Hardware
- counter
- counterPulse
- eventCounter
- pipe
- Bus
  - Bus.pipe

Theorems

⊦ ∀ld nb dn t. signal ld t ∧ counter ld nb dn ⇒ ¬signal dn t

⊦ ∀ld nb dn t. signal ld t ∧ counterPulse ld nb dn ⇒ ¬signal dn t

⊦ ∀ld nb dn. counterPulse ld nb dn ⇔ ∃ds. counter ld nb ds ∧ pulse ds dn

⊦ ∀w d wd t. pipe w d wd ⇒ (signal wd (t + d) ⇔ signal w t)

⊦ ∀w x i xi t.
Bus.pipe w x ∧ Bus.wire x i xi ⇒ (signal xi (t + i) ⇔ signal w t)

⊦ ∀w d wd.
    pipe w d wd ⇔
    ∃x x₀.
      Bus.width x = d + 1 ∧ Bus.wire x d x₀ ∧ Bus.pipe w x ∧ connect x₀ wd

⊦ ∀w x.
    Bus.pipe w x ⇔
    ∃r xp x₀ x₁ x₂.
      Bus.width x = r + 1 ∧ Bus.width xp = r ∧ Bus.wire x 0 x₀ ∧
      Bus.sub x 0 r x₁ ∧ Bus.sub x 1 r x₂ ∧ connect w x₀ ∧
      Bus.connect xp x₂ ∧ Bus.delay x₁ xp

⊦ ∀n ld nb dn t k.
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal nb t) + (n + 2) =
    2 ↑ Bus.width nb + Bus.width nb ∧ counter ld nb dn ⇒
    (signal dn (t + k) ⇔ n < k)

⊦ ∀n ld nb dn t k.
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal nb t) + (n + 2) =
    2 ↑ Bus.width nb + Bus.width nb ∧ counterPulse ld nb dn ⇒
    (signal dn (t + k) ⇔ k = n + 1)

⊦ ∀n ld nb inc dn t k.
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal nb t) + n = 2 ↑ Bus.width nb ∧
    eventCounter ld nb inc dn ⇒
    (signal dn (t + k) ⇔
     n ≤ size { i. i | 0 < i ∧ i + Bus.width nb ≤ k ∧ signal inc (t + i) })

⊦ ∀ld nb dn.
    counter ld nb dn ⇔
    ∃r sp cp sq cq sr cr dp dq dr nb₀ nb₁ cp₀ cp₁ cp₂ cq₀ cq₁ cr₀ cr₁.
      Bus.width nb = r + 1 ∧ Bus.width sp = r ∧ Bus.width cp = r + 1 ∧
      Bus.width sq = r ∧ Bus.width cq = r + 1 ∧ Bus.width sr = r ∧
      Bus.width cr = r + 1 ∧ Bus.wire nb 0 nb₀ ∧ Bus.sub nb 1 r nb₁ ∧
      Bus.wire cp 0 cp₀ ∧ Bus.sub cp 0 r cp₁ ∧ Bus.wire cp r cp₂ ∧
      Bus.wire cq 0 cq₀ ∧ Bus.sub cq 1 r cq₁ ∧ Bus.wire cr 0 cr₀ ∧
      Bus.sub cr 1 r cr₁ ∧ not cp₀ cq₀ ∧ Bus.adder2 sp cp₁ sq cq₁ ∧
      or2 dp cp₂ dq ∧ Bus.case1 ld nb₁ sq sr ∧ case1 ld nb₀ cq₀ cr₀ ∧
      Bus.case1 ld (Bus.ground r) cq₁ cr₁ ∧ case1 ld ground dq dr ∧
      connect dr dn ∧ Bus.delay sr sp ∧ Bus.delay cr cp ∧ delay dr dp

⊦ ∀ld nb inc dn.
    eventCounter ld nb inc dn ⇔
    ∃r sp cp sq cq sr cr dp dq dr sp₀ sp₁ cp₀ cp₁ cp₂ sq₀ sq₁ cq₀ cq₁.
      Bus.width nb = r + 1 ∧ Bus.width sp = r + 1 ∧ Bus.width cp = r + 1 ∧
      Bus.width sq = r + 1 ∧ Bus.width cq = r + 1 ∧ Bus.width sr = r + 1 ∧
      Bus.width cr = r + 1 ∧ Bus.wire sp 0 sp₀ ∧ Bus.sub sp 1 r sp₁ ∧
      Bus.wire sq 0 sq₀ ∧ Bus.sub sq 1 r sq₁ ∧ Bus.wire cp 0 cp₀ ∧
      Bus.sub cp 0 r cp₁ ∧ Bus.wire cp r cp₂ ∧ Bus.wire cq 0 cq₀ ∧
      Bus.sub cq 1 r cq₁ ∧ xor2 inc sp₀ sq₀ ∧ and2 inc sp₀ cq₀ ∧
      Bus.adder2 sp₁ cp₁ sq₁ cq₁ ∧ or2 dp cp₂ dq ∧ Bus.case1 ld nb sq sr ∧
      Bus.case1 ld (Bus.ground (r + 1)) cq cr ∧ case1 ld ground dq dr ∧
      connect dr dn ∧ Bus.delay sr sp ∧ Bus.delay cr cp ∧ delay dr dp

External Type Operators

→
bool
Data
- List
  - list
- Pair
  - ×
- Stream
  - stream
Hardware
- bus
- wire
Number
- Natural
  - natural
Set
- set

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - @
  - []
  - length
  - map
- Pair
  - ,
  - fst
  - snd
- Stream
  - fromFunction
  - nth
Function
- ∘
Hardware
- and2
- bus
- case1
- connect
- delay
- ground
- not
- or2
- power
- pulse
- signal
- signals
- wire
- xor2
- Bus
  - Bus.adder2
  - Bus.and2
  - Bus.append
  - Bus.case1
  - Bus.connect
  - Bus.delay
  - Bus.ground
  - Bus.lift2
  - Bus.lift3
  - Bus.nil
  - Bus.signal
  - Bus.single
  - Bus.sub
  - Bus.width
  - Bus.wire
  - Bus.wires
  - Bus.xor2
Number
- Natural
  - *
  - +
  - -
  - <
  - ≤
  - ↑
  - bit0
  - bit1
  - fromBool
  - minimal
  - suc
  - zero
  - Bits
    - Bits.cons
    - Bits.shiftLeft
    - Bits.toNatural
Set
- ∅
- disjoint
- finite
- fromPredicate
- image
- insert
- ∩
- ∈
- size
- ⊆
- ∪

Assumptions

⊦ ⊤

⊦ finite ∅

⊦ Bus.nil = bus []

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ bit0 0 = 0

⊦ fromBool ⊥ = 0

⊦ size ∅ = 0

⊦ ∀t. t ⇒ t

⊦ ∀x. connect x x

⊦ ∀t. signal power t

⊦ ∀n. 0 ≤ n

⊦ ∀n. n ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ fromPredicate (λx. ⊥) = ∅

⊦ fromBool ⊤ = 1

⊦ ∀x. ¬(x ∈ ∅)

⊦ ∀t. t ∨ ¬t

⊦ ∀t. ¬signal ground t

⊦ ∀m. ¬(m < 0)

⊦ ∀n. ¬(n < n)

⊦ ∀n. 0 < suc n

⊦ ∀n. n < suc n

⊦ ∀n. n ≤ suc n

⊦ (¬) = λp. p ⇒ ⊥

⊦ ∀a. ∃x. x = a

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

⊦ ∀x. ∃y. Bus.delay x y

⊦ ∀x. ∃y. connect x y

⊦ ∀x. ∃y. delay x y

⊦ ∀x. ∃y. not 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. ⊤ ∨ t ⇔ ⊤

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. Bus.width (Bus.ground n) = n

⊦ ∀m. m * 0 = 0

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀m. m - 0 = m

⊦ ∀k. Bits.shiftLeft 0 k = 0

⊦ ∀l. Bus.wires (bus l) = l

⊦ ∀s. signals (wire s) = s

⊦ ∀f. map f [] = []

⊦ ∀f. nth (fromFunction f) = f

⊦ (∘) = λf g x. f (g x)

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀w. signal w = nth (signals w)

⊦ ∀s. Bus.case1 s = Bus.lift3 (case1 s)

⊦ ∀w. Bus.width (Bus.single w) = 1

⊦ ∀n. bit1 n = suc (bit0 n)

⊦ ∀m. m * 1 = m

⊦ ∀m n. m ≤ m + n

⊦ ∀m n. n ≤ m + n

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀x. size (insert x ∅) = 1

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀b. fromBool b = 0 ⇔ ¬b

⊦ ∀b. Bits.toNatural (b :: []) = fromBool b

⊦ ∀x y. ∃z. or2 x y z

⊦ ∀w. Bus.single w = bus (w :: [])

⊦ ∀m. suc m = m + 1

⊦ ∀m. m ≤ 0 ⇔ m = 0

⊦ ∀n. suc n - 1 = n

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

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

⊦ ∀a b. fst (a, b) = a

⊦ ∀a b. snd (a, b) = b

⊦ ∀n. 0 < n ⇔ ¬(n = 0)

⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))

⊦ ∀x. ∃a b. x = (a, b)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀t₁ t₂. t₁ ∨ t₂ ⇔ t₂ ∨ t₁

⊦ ∀x t. length (Bus.signal x t) = Bus.width x

⊦ ∀m n. m + n = n + m

⊦ ∀m n. m < n ⇒ m ≤ n

⊦ ∀n t. Bits.toNatural (Bus.signal (Bus.ground n) t) = 0

⊦ ∀m n. m + n - m = n

⊦ ∀m n. m + n - n = m

⊦ ∀s x. finite (insert x s) ⇔ finite s

⊦ ∀p x. x ∈ fromPredicate p ⇔ p x

⊦ ∅ = { x. x | ⊥ }

⊦ ∀n. Bits.cons ⊥ n = 2 * n

⊦ ∀l. Bits.toNatural l < 2 ↑ length l

⊦ ∀x y. connect x y ⇒ and2 power x y

⊦ ∀x y. not x y ⇒ xor2 power x y

⊦ ∀m n. ¬(m < n) ⇔ n ≤ m

⊦ ∀m n. ¬(m ≤ n) ⇔ n < m

⊦ ∀m n. m < suc n ⇔ m ≤ n

⊦ ∀m n. suc m ≤ n ⇔ m < n

⊦ ∀m. m = 0 ∨ ∃n. m = suc n

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ ∀n. Bits.shiftLeft n 1 = 2 * n

⊦ ∀p. ¬(∃x. p x) ⇔ ∀x. ¬p x

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀x y. x ∈ insert y ∅ ⇔ x = y

⊦ ∀h t. (h :: []) @ t = h :: t

⊦ ∀t₁ t₂. ¬t₁ ⇒ ¬t₂ ⇔ t₂ ⇒ t₁

⊦ ∀h t. Bits.toNatural (h :: t) = Bits.cons h (Bits.toNatural t)

⊦ ∀m n. m + suc n = suc (m + n)

⊦ ∀m n. suc m + n = suc (m + n)

⊦ ∀m n. m < m + n ⇔ 0 < n

⊦ ∀m n. n < m + n ⇔ 0 < m

⊦ ∀m n. suc m = suc n ⇔ m = n

⊦ ∀m n. suc m < suc n ⇔ m < n

⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n

⊦ ∀m n. m + n = m ⇔ n = 0

⊦ ∀k n. Bits.shiftLeft n k = 0 ⇔ n = 0

⊦ ∀m n. m + n ≤ m ⇔ n = 0

⊦ ∀m n. n + m ≤ m ⇔ n = 0

⊦ ∀s t. disjoint s t ⇔ s ∩ t = ∅

⊦ ∀s t. finite t ∧ s ⊆ t ⇒ finite s

⊦ ∀n. finite { m. m | m ≤ n }

⊦ ∀x y. Bus.append x y = bus (Bus.wires x @ Bus.wires y)

⊦ ∀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 = signal w t :: []

⊦ ∀w t.
Bits.toNatural (Bus.signal (Bus.single w) t) = fromBool (signal w t)

⊦ ∀m n. m ↑ suc n = m * m ↑ n

⊦ ∀x i w. Bus.wire x i w ⇒ i < Bus.width x

⊦ ∀x t. Bus.signal x t = map (λw. signal w t) (Bus.wires x)

⊦ ∀x i. i < Bus.width x ⇒ ∃w. Bus.wire x i w

⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d

⊦ ∀p a. (∃x. a = x ∧ p x) ⇔ p a

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n

⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n

⊦ ∀m n. m < n ⇔ ∃d. n = m + suc d

⊦ ∀h t. Bits.cons h t = fromBool h + 2 * t

⊦ ∀p q. (∀x. p ⇒ q x) ⇔ p ⇒ ∀x. q x

⊦ ∀a b. a ⊆ b ∧ finite b ⇒ size a ≤ size b

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

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

⊦ ∀m n p. m + n < m + p ⇔ n < p

⊦ ∀m n p. n + m < p + m ⇔ n < p

⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p

⊦ ∀m n p. n + m ≤ p + m ⇔ n ≤ p

⊦ ∀k n₁ n₂. Bits.shiftLeft n₁ k ≤ Bits.shiftLeft n₂ k ⇔ n₁ ≤ n₂

⊦ ∀m n p. m < n ∧ n < p ⇒ m < p

⊦ ∀m n p. m < n ∧ n ≤ p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n < p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

⊦ ∀s t. s ⊆ t ⇔ ∀x. x ∈ s ⇒ x ∈ t

⊦ ∀s t. (∀x. x ∈ s ⇔ x ∈ t) ⇔ s = t

⊦ ∀p x. (∀y. p y ⇔ y = x) ⇒ (select) p = x

⊦ ∀f g l. map (f ∘ g) l = map f (map g l)

⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)

⊦ ∀r. (∀xi. ∃yi. r xi yi) ⇒ ∀x. ∃y. Bus.lift2 r x y

⊦ ∀x k n y. Bus.sub x k n y ⇒ Bus.width y = n

⊦ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n

⊦ ∀x i w. Bus.wire x i w ⇔ Bus.sub x i 1 (Bus.single w)

⊦ ∀x y t. not x y ⇒ (signal y t ⇔ ¬signal x t)

⊦ ∀f h t. map f (h :: t) = f h :: map f t

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

⊦ ∀x y. Bus.width x = Bus.width y ⇒ ∃s c. Bus.adder2 x y s c

⊦ ∀p x. x ∈ { y. y | p y } ⇔ p x

⊦ ∀x y s. x ∈ insert y s ⇔ x = y ∨ x ∈ s

⊦ ∀p q r. p ∧ (q ∨ r) ⇔ p ∧ q ∨ p ∧ r

⊦ ∀p q r. (p ∨ q) ∧ r ⇔ p ∧ r ∨ q ∧ r

⊦ ∀x y z. Bus.sub (Bus.append x y) (Bus.width x) (Bus.width y) z ⇔ z = y

⊦ ∀x y n. Bus.delay x y ∧ Bus.width x = n ⇒ Bus.width y = n

⊦ ∀x y t. pulse x y ∧ ¬signal x t ⇒ ¬signal y t

⊦ ∀n k w. Bus.wire (Bus.ground n) k w ⇔ k < n ∧ w = ground

⊦ ∀m n p. m * (n + p) = m * n + m * p

⊦ ∀n. size { m. m | m ≤ n } = n + 1

⊦ ∀s t x. x ∈ s ∩ t ⇔ x ∈ s ∧ x ∈ t

⊦ ∀s t x. x ∈ s ∪ t ⇔ x ∈ s ∨ x ∈ t

⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y

⊦ ∀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 =
signal w t :: Bus.signal x t

⊦ ∀x y t. delay x y ⇒ (signal y (t + 1) ⇔ signal x t)

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n

⊦ ∀x i w₁ w₂. Bus.wire x i w₁ ∧ Bus.wire x i w₂ ⇒ w₁ = w₂

⊦ ∀m n p. m * n = m * p ⇔ m = 0 ∨ n = p

⊦ ∀p n. p n ∧ (∀m. m < n ⇒ ¬p m) ⇒ (minimal) p = n

⊦ ∀p. (∃n. p n) ⇔ p ((minimal) p) ∧ ∀m. m < (minimal) p ⇒ ¬p m

⊦ ∀y s f. y ∈ image f s ⇔ ∃x. y = f x ∧ x ∈ s

⊦ ∀r x y n. Bus.lift2 r x y ∧ Bus.width x = n ⇒ Bus.width y = n

⊦ ∀m n p. m * n < m * p ⇔ ¬(m = 0) ∧ n < p

⊦ ∀a b a' b'. (a, b) = (a', b') ⇔ a = a' ∧ b = b'

⊦ ∀h₁ h₂ t₁ t₂. Bits.cons h₁ t₁ = Bits.cons h₂ t₂ ⇔ (h₁ ⇔ h₂) ∧ t₁ = t₂

⊦ ∀x y s c. Bus.adder2 x y s c ⇔ Bus.xor2 x y s ∧ Bus.and2 x y c

⊦ ∀x y z t. and2 x y z ⇒ (signal z t ⇔ signal x t ∧ signal y t)

⊦ ∀x y z t. or2 x y z ⇒ (signal z t ⇔ signal x t ∨ signal y t)

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀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 t. xor2 x y z ⇒ (signal z t ⇔ ¬(signal x t ⇔ signal y t))

⊦ ∀n i k x. Bus.sub (Bus.ground n) i k x ⇔ i + k ≤ n ∧ x = Bus.ground k

⊦ ∀s t. finite s ∧ finite t ∧ disjoint s t ⇒ size (s ∪ t) = size s + size t

⊦ ∀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 i xi yi.
Bus.connect x y ∧ Bus.wire x i xi ∧ Bus.wire y i yi ⇒ connect xi yi

⊦ ∀x y i xi yi.
Bus.delay x y ∧ Bus.wire x i xi ∧ Bus.wire y i yi ⇒ delay xi yi

⊦ ∀x i w t.
Bus.wire x i w ∧ signal w t ⇒ 2 ↑ i ≤ Bits.toNatural (Bus.signal x t)

⊦ ∀x y t. pulse x y ⇒ (signal y (t + 1) ⇔ ¬signal x t ∧ signal x (t + 1))

⊦ ∀r x y i xi yi.
Bus.lift2 r x y ∧ Bus.wire x i xi ∧ Bus.wire y i yi ⇒ r xi yi

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

⊦ ∀s x y z.
case1 s x y z ⇔
∀t. signal z t ⇔ if signal s t then signal x t else signal y t

⊦ ∀x y k n xs ys.
Bus.delay x y ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ⇒ Bus.delay xs ys

⊦ ∀x k n y i w.
Bus.sub x k n y ⇒ (Bus.wire y i w ⇔ i < n ∧ Bus.wire x (k + i) w)

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

⊦ ∀f s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ∧ finite s ⇒
size (image f s) = size s

⊦ ∀x y z i xi yi zi.
Bus.and2 x y z ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧ Bus.wire z i zi ⇒
and2 xi yi zi

⊦ ∀x y z i xi yi zi.
Bus.xor2 x y z ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧ Bus.wire z i zi ⇒
xor2 xi yi zi

⊦ ∀x j m y k n z.
Bus.sub x j m y ⇒ (Bus.sub y k n z ⇔ k + n ≤ m ∧ Bus.sub x (j + k) n z)

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

⊦ ∀s x y z i xi yi zi.
Bus.case1 s x y z ∧ Bus.wire x i xi ∧ Bus.wire y i yi ∧
Bus.wire z i zi ⇒ case1 s xi yi zi

⊦ ∀s x y z k n xs ys zs.
Bus.case1 s x y z ∧ Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.sub z k n zs ⇒ Bus.case1 s xs ys zs

⊦ ∀r p.
    p Bus.nil Bus.nil ∧
    (∀xh xt yh yt.
       r xh yh ∧ Bus.lift2 r xt yt ∧ p xt yt ⇒
       p (Bus.append (Bus.single xh) xt) (Bus.append (Bus.single yh) yt)) ⇒
    ∀x y. Bus.lift2 r x y ⇒ p x y

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

⊦ ∀r x y z.
    Bus.lift3 r x y z ⇔
    ∃n.
      Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n ∧
      ∀i xi yi zi.
        Bus.wire x i xi ∧ Bus.wire y i yi ∧ Bus.wire z i zi ⇒ r xi yi zi