Package char: Theory of Unicode characters

Information

Files

• Package tarball char-1.4.tgz
• Theory file char.thy (included in the package tarball)

Defined Type Operators

• Data
  • Char
    • char
    • plane
    • position

Defined Constants

• Data
  • Char
    • destChar
    • destPlane
    • destPosition
    • isChar
    • isPlane
    • isPosition
    • mkChar
    • mkPlane
    • mkPosition
    • UTF8
      • UTF8.decode
      • UTF8.decodeStream
      • UTF8.decoder
        • UTF8.decoder.decode1
        • UTF8.decoder.decode2
        • UTF8.decoder.decode3
        • UTF8.decoder.parse
      • UTF8.encode
      • UTF8.encoder
        • UTF8.encoder.encode1
        • UTF8.encoder.encode2
        • UTF8.encoder.encode3
      • UTF8.isContinuationByte
      • UTF8.parseContinuationByte
      • UTF8.parseThreeContinuationBytes
      • UTF8.parseTwoContinuationBytes

Theorems

⊦ isParser UTF8.decoder.parse

⊦ inverse UTF8.decoder UTF8.encoder

⊦ UTF8.parseContinuationByte = parseSome UTF8.isContinuationByte

⊦ UTF8.decoder = mkParser UTF8.decoder.parse

⊦ UTF8.decodeStream = parseStream UTF8.decoder

⊦ destParser UTF8.decoder = UTF8.decoder.parse

⊦ UTF8.parseTwoContinuationBytes =
  parsePair UTF8.parseContinuationByte UTF8.parseContinuationByte

⊦ UTF8.parseThreeContinuationBytes =
  parsePair UTF8.parseContinuationByte UTF8.parseTwoContinuationBytes

⊦ ∀p. isPosition p ⇔ T

⊦ parse UTF8.decoder =
  Stream.case Data.Option.none Data.Option.none UTF8.decoder.parse

⊦ ∀bs.
    UTF8.decode bs = Stream.toList (UTF8.decodeStream (Stream.fromList bs))

⊦ ∀chs. UTF8.encode chs = concat (map UTF8.encoder chs)

⊦ ∀pl. ∃b. isPlane b ∧ pl = mkPlane b

⊦ ∀pos. ∃w. isPosition w ∧ pos = mkPosition w

⊦ ∀p. isPlane p ⇔ Byte.< p (Byte.fromNatural 17)

⊦ ∀pl. ∃b. isPlane b ∧ pl = mkPlane b ∧ destPlane pl = b

⊦ ∀pos. ∃w. isPosition w ∧ pos = mkPosition w ∧ destPosition pos = w

⊦ ∀c. ∃pl pos. isChar (pl, pos) ∧ c = mkChar (pl, pos)

⊦ (∀a. mkChar (destChar a) = a) ∧ ∀r. isChar r ⇔ destChar (mkChar r) = r

⊦ (∀a. mkPlane (destPlane a) = a) ∧
  ∀r. isPlane r ⇔ destPlane (mkPlane r) = r

⊦ (∀a. mkPosition (destPosition a) = a) ∧
  ∀r. isPosition r ⇔ destPosition (mkPosition r) = r

⊦ ∀b. UTF8.isContinuationByte b ⇔ Byte.bit b 7 ∧ ¬Byte.bit b 6

⊦ ∀c.
    ∃pl pos.
      isChar (pl, pos) ∧ c = mkChar (pl, pos) ∧ destChar c = (pl, pos)

⊦ ∀p0 p1.
    UTF8.encoder.encode1 p0 p1 =
    let b00 = Byte.shiftLeft p0 2 in
    let b01 = Byte.shiftRight (Byte.and p1 (Byte.fromNatural 192)) 6 in
    let b0 = Byte.or (Byte.fromNatural 192) (Byte.or b00 b01) in
    let b10 = Byte.and p1 (Byte.fromNatural 63) in
    let b1 = Byte.or (Byte.fromNatural 128) b10 in
    b0 :: b1 :: []

⊦ ∀ch.
    UTF8.encoder ch =
    let (pl, pos) = destChar ch in
    let p = destPlane pl in
    let (p0, p1) = Word16.toBytes (destPosition pos) in
    if p = Byte.fromNatural 0 then
      if p0 = Byte.fromNatural 0 ∧ ¬Byte.bit p1 7 then p1 :: []
      else if Byte.and (Byte.fromNatural 248) p0 = Byte.fromNatural 0 then
        UTF8.encoder.encode1 p0 p1
      else UTF8.encoder.encode2 p0 p1
    else UTF8.encoder.encode3 p p0 p1

⊦ ∀b0 s.
    UTF8.decoder.parse b0 s =
    if Byte.bit b0 7 then
      if Byte.bit b0 6 then
        if Byte.bit b0 5 then
          if Byte.bit b0 4 then
            if Byte.bit b0 3 then Data.Option.none
            else
              parse
                (partialMap (UTF8.decoder.decode3 b0)
                   UTF8.parseThreeContinuationBytes) s
          else
            parse
              (partialMap (UTF8.decoder.decode2 b0)
                 UTF8.parseTwoContinuationBytes) s
        else
          parse
            (partialMap (UTF8.decoder.decode1 b0)
               UTF8.parseContinuationByte) s
      else Data.Option.none
    else
      let pl = mkPlane (Byte.fromNatural 0) in
      let pos = mkPosition (Word16.fromBytes (Byte.fromNatural 0) b0) in
      let ch = mkChar (pl, pos) in
      Data.Option.some (ch, s)

⊦ ∀pl pos.
    isChar (pl, pos) ⇔
    let pli = destPlane pl in
    let posi = destPosition pos in
    ¬(pli = Byte.fromNatural 0) ∨
    Word16.< posi (Word16.fromNatural 55296) ∨
    Word16.< (Word16.fromNatural 57343) posi ∧
    Word16.< posi (Word16.fromNatural 65534)

⊦ ∀b0 b1.
    UTF8.decoder.decode1 b0 b1 =
    let pl = mkPlane (Byte.fromNatural 0) in
    let p0 = Byte.shiftRight (Byte.and b0 (Byte.fromNatural 28)) 2 in
    let y1 = Byte.shiftLeft (Byte.and b0 (Byte.fromNatural 3)) 6 in
    let x1 = Byte.and b1 (Byte.fromNatural 63) in
    let p1 = Byte.or y1 x1 in
    if p0 = Byte.fromNatural 0 ∧ Byte.< p1 (Byte.fromNatural 128) then
      Data.Option.none
    else
      let pos = mkPosition (Word16.fromBytes p0 p1) in
      let ch = mkChar (pl, pos) in
      Data.Option.some ch

⊦ ∀p0 p1.
    UTF8.encoder.encode2 p0 p1 =
    let b00 = Byte.shiftRight (Byte.and p0 (Byte.fromNatural 240)) 4 in
    let b0 = Byte.or (Byte.fromNatural 224) b00 in
    let b10 = Byte.shiftLeft (Byte.and p0 (Byte.fromNatural 15)) 2 in
    let b11 = Byte.shiftRight (Byte.and p1 (Byte.fromNatural 192)) 6 in
    let b1 = Byte.or (Byte.fromNatural 128) (Byte.or b10 b11) in
    let b20 = Byte.and p1 (Byte.fromNatural 63) in
    let b2 = Byte.or (Byte.fromNatural 128) b20 in
    b0 :: b1 :: b2 :: []

⊦ ∀b0 b1 b2 b3.
    UTF8.decoder.decode3 b0 (b1, b2, b3) =
    let w = Byte.shiftLeft (Byte.and b0 (Byte.fromNatural 7)) 2 in
    let z = Byte.shiftRight (Byte.and b1 (Byte.fromNatural 48)) 4 in
    let p = Byte.or w z in
    if p = Byte.fromNatural 0 ∨ Byte.< (Byte.fromNatural 16) p then
      Data.Option.none
    else
      let pl = mkPlane p in
      let z0 = Byte.shiftLeft (Byte.and b1 (Byte.fromNatural 15)) 4 in
      let y0 = Byte.shiftRight (Byte.and b2 (Byte.fromNatural 60)) 2 in
      let p0 = Byte.or z0 y0 in
      let y1 = Byte.shiftLeft (Byte.and b2 (Byte.fromNatural 3)) 6 in
      let x1 = Byte.and b3 (Byte.fromNatural 63) in
      let p1 = Byte.or y1 x1 in
      let pos = mkPosition (Word16.fromBytes p0 p1) in
      let ch = mkChar (pl, pos) in
      Data.Option.some ch

⊦ ∀b0 b1 b2.
    UTF8.decoder.decode2 b0 (b1, b2) =
    let z0 = Byte.shiftLeft (Byte.and b0 (Byte.fromNatural 15)) 4 in
    let y0 = Byte.shiftRight (Byte.and b1 (Byte.fromNatural 60)) 2 in
    let p0 = Byte.or z0 y0 in
    if Byte.< p0 (Byte.fromNatural 8) ∨
       Byte.≤ (Byte.fromNatural 216) p0 ∧ Byte.≤ p0 (Byte.fromNatural 223)
    then Data.Option.none
    else
      let y1 = Byte.shiftLeft (Byte.and b1 (Byte.fromNatural 3)) 6 in
      let x1 = Byte.and b2 (Byte.fromNatural 63) in
      let p1 = Byte.or y1 x1 in
      if p0 = Byte.fromNatural 255 ∧ Byte.≤ (Byte.fromNatural 254) p1 then
        Data.Option.none
      else
        let pl = mkPlane (Byte.fromNatural 0) in
        let pos = mkPosition (Word16.fromBytes p0 p1) in
        let ch = mkChar (pl, pos) in
        Data.Option.some ch

⊦ ∀p p0 p1.
    UTF8.encoder.encode3 p p0 p1 =
    let b00 = Byte.shiftRight (Byte.and p (Byte.fromNatural 28)) 2 in
    let b0 = Byte.or (Byte.fromNatural 240) b00 in
    let b10 = Byte.shiftLeft (Byte.and p (Byte.fromNatural 3)) 4 in
    let b11 = Byte.shiftRight (Byte.and p0 (Byte.fromNatural 240)) 4 in
    let b1 = Byte.or (Byte.fromNatural 128) (Byte.or b10 b11) in
    let b20 = Byte.shiftLeft (Byte.and p0 (Byte.fromNatural 15)) 2 in
    let b21 = Byte.shiftRight (Byte.and p1 (Byte.fromNatural 192)) 6 in
    let b2 = Byte.or (Byte.fromNatural 128) (Byte.or b20 b21) in
    let b30 = Byte.and p1 (Byte.fromNatural 63) in
    let b3 = Byte.or (Byte.fromNatural 128) b30 in
    b0 :: b1 :: b2 :: b3 :: []

Input Type Operators

• →
• bool
• Data
  • Byte
    • Byte.byte
  • List
    • list
  • Option
    • Data.Option.option
  • Pair
    • *
  • Word16
    • Word16.word16
• Number
  • Natural
    • Number.Natural.natural
• Parser
  • parser
  • Stream
    • Stream.stream

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • cond
    • let
    • select
    • F
    • T
  • Byte
    • Byte.+
    • Byte.<
    • Byte.≤
    • Byte.and
    • Byte.bit
    • Byte.fromNatural
    • Byte.modulus
    • Byte.or
    • Byte.shiftLeft
    • Byte.shiftRight
    • Byte.toNatural
    • Byte.width
    • Bits
      • Byte.Bits.compare
      • Byte.Bits.fromWord
      • Byte.Bits.toWord
  • List
    • ::
    • @
    • []
    • concat
    • drop
    • length
    • map
    • nth
    • replicate
    • take
    • zipWith
  • Option
    • Data.Option.case
    • Data.Option.none
    • Data.Option.some
  • Pair
    • ,
    • fst
    • snd
  • Word16
    • Word16.+
    • Word16.<
    • Word16.fromBytes
    • Word16.fromNatural
    • Word16.shiftLeft
    • Word16.toBytes
    • Word16.width
    • Bits
      • Word16.Bits.compare
      • Word16.Bits.fromWord
      • Word16.Bits.toWord
• Number
  • Natural
    • Number.Natural.*
    • Number.Natural.+
    • Number.Natural.-
    • Number.Natural.<
    • Number.Natural.≤
    • Number.Natural.div
    • Number.Natural.even
    • Number.Natural.exp
    • Number.Natural.mod
    • Number.Natural.odd
    • Number.Natural.suc
  • Numeral
    • bit0
    • bit1
    • zero
• Parser
  • destParser
  • inverse
  • isParser
  • mkParser
  • parse
  • parsePair
  • parseSome
  • parseStream
  • partialMap
  • Stream
    • Stream.append
    • Stream.case
    • Stream.eof
    • Stream.error
    • Stream.fromList
    • Stream.isProperSuffix
    • Stream.isSuffix
    • Stream.stream
    • Stream.toList

Assumptions

⊦ T

⊦ ∀n. Number.Natural.≤ 0 n

⊦ ∀x. Stream.isSuffix x x

⊦ F ⇔ ∀p. p

⊦ let = λf x. f x

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ F

⊦ (∃) = λP. P ((select) P)

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

⊦ ∀t. (λx. t x) = t

⊦ (∀) = λP. P = λx. T

⊦ ∀a'. ¬(Data.Option.none = Data.Option.some a')

⊦ ∀x. x = x ⇔ T

⊦ ∀n. ¬(Number.Natural.suc n = 0)

⊦ Byte.modulus = Number.Natural.exp 2 Byte.width

⊦ Byte.width = 8

⊦ ∀n. bit0 n = Number.Natural.+ n n

⊦ Word16.width = 16

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

⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)

⊦ ∀n. bit1 n = Number.Natural.suc (Number.Natural.+ n n)

⊦ ∀x.
    Byte.toNatural (Byte.fromNatural x) = Number.Natural.mod x Byte.modulus

⊦ ∀x. (fst x, snd x) = x

⊦ ∀x y. fst (x, y) = x

⊦ ∀x y. snd (x, y) = y

⊦ ∀P x. P x ⇒ P ((select) P)

⊦ (¬T ⇔ F) ∧ (¬F ⇔ T)

⊦ ∀f y. (λx. f x) y = f y

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

⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1

⊦ ∀m n. Number.Natural.- (Number.Natural.+ m n) n = m

⊦ ∀x y. Stream.isProperSuffix x y ⇒ Stream.isSuffix x y

⊦ ∀n. Number.Natural.* 2 n = Number.Natural.+ n n

⊦ ∀x y. Byte.< x y ⇔ ¬Byte.≤ y x

⊦ ∀m n. ¬Number.Natural.≤ m n ⇔ Number.Natural.< n m

⊦ ∀m n. Number.Natural.≤ (Number.Natural.suc m) n ⇔ Number.Natural.< m n

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

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

⊦ ∀x y. Byte.≤ x y ⇔ Number.Natural.≤ (Byte.toNatural x) (Byte.toNatural y)

⊦ ∀w1 w2. Byte.Bits.fromWord w1 = Byte.Bits.fromWord w2 ⇔ w1 = w2

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

⊦ ∀m n. Number.Natural.- m n = 0 ⇔ Number.Natural.≤ m n

⊦ ∀w1 w2.
    Byte.Bits.compare F (Byte.Bits.fromWord w1) (Byte.Bits.fromWord w2) ⇔
    Byte.< w1 w2

⊦ ∀w1 w2.
    Byte.Bits.compare T (Byte.Bits.fromWord w1) (Byte.Bits.fromWord w2) ⇔
    Byte.≤ w1 w2

⊦ ∀b0 b1.
    Word16.Bits.toWord (Byte.Bits.fromWord b1 @ Byte.Bits.fromWord b0) =
    Word16.fromBytes b0 b1

⊦ ∀w1 w2.
    Word16.Bits.compare F (Word16.Bits.fromWord w1)
      (Word16.Bits.fromWord w2) ⇔ Word16.< w1 w2

⊦ ∀m n.
    Number.Natural.even (Number.Natural.* m n) ⇔
    Number.Natural.even m ∨ Number.Natural.even n

⊦ ∀m n.
    Number.Natural.even (Number.Natural.+ m n) ⇔ Number.Natural.even m ⇔
    Number.Natural.even n

⊦ ∀f g. f = g ⇔ ∀x. f x = g x

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

⊦ (Number.Natural.even 0 ⇔ T) ∧
  ∀n. Number.Natural.even (Number.Natural.suc n) ⇔ ¬Number.Natural.even n

⊦ (Number.Natural.odd 0 ⇔ F) ∧
  ∀n. Number.Natural.odd (Number.Natural.suc n) ⇔ ¬Number.Natural.odd n

⊦ ∀w1 w2.
    Byte.and w1 w2 =
    Byte.Bits.toWord
      (zipWith (∧) (Byte.Bits.fromWord w1) (Byte.Bits.fromWord w2))

⊦ ∀w1 w2.
    Byte.or w1 w2 =
    Byte.Bits.toWord
      (zipWith (∨) (Byte.Bits.fromWord w1) (Byte.Bits.fromWord w2))

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

⊦ ∀m n.
    Number.Natural.odd (Number.Natural.+ m n) ⇔
    ¬(Number.Natural.odd m ⇔ Number.Natural.odd n)

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

⊦ ∀l n.
    Byte.shiftLeft (Byte.Bits.toWord l) n =
    Byte.Bits.toWord (replicate n F @ l)

⊦ ∀PAIR'. ∃fn. ∀a0 a1. fn (a0, a1) = PAIR' a0 a1

⊦ ∀t1 t2 t3. t1 ∨ t2 ∨ t3 ⇔ (t1 ∨ t2) ∨ t3

⊦ ∀n.
    Byte.Bits.toWord
      (Number.Natural.odd n ::
       Byte.Bits.fromWord (Byte.fromNatural (Number.Natural.div n 2))) =
    Byte.fromNatural n

⊦ ∀n.
    Word16.Bits.toWord
      (Number.Natural.odd n ::
       Word16.Bits.fromWord
         (Word16.fromNatural (Number.Natural.div n 2))) =
    Word16.fromNatural n

⊦ ∀t1 t2. (if T then t1 else t2) = t1 ∧ (if F then t1 else t2) = t2

⊦ ∀x y.
    Byte.fromNatural x = Byte.fromNatural y ⇔
    Number.Natural.mod x Byte.modulus = Number.Natural.mod y Byte.modulus

⊦ ∀m n. Number.Natural.* m n = 0 ⇔ m = 0 ∨ n = 0

⊦ length [] = 0 ∧ ∀h t. length (h :: t) = Number.Natural.suc (length t)

⊦ ∀w. ∃b0 b1. w = Word16.fromBytes b0 b1 ∧ Word16.toBytes w = (b0, b1)

⊦ (∀t. ¬¬t ⇔ t) ∧ (¬T ⇔ F) ∧ (¬F ⇔ T)

⊦ (∀a. mkParser (destParser a) = a) ∧
  ∀r. isParser r ⇔ destParser (mkParser r) = r

⊦ ∀b t1 t2. (if b then t1 else t2) ⇔ (¬b ∨ t1) ∧ (b ∨ t2)

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

⊦ ∀m n p.
    Number.Natural.exp m (Number.Natural.+ n p) =
    Number.Natural.* (Number.Natural.exp m n) (Number.Natural.exp m p)

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

⊦ ∀x. x = Stream.error ∨ x = Stream.eof ∨ ∃a0 a1. x = Stream.stream a0 a1

⊦ ∀p.
    parse (parseSome p) =
    Stream.case Data.Option.none Data.Option.none
      (λa s. if p a then Data.Option.some (a, s) else Data.Option.none)

⊦ ∀b f x y. f (if b then x else y) = if b then f x else f y

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

⊦ ∀m n p.
    Number.Natural.≤ (Number.Natural.* m n) (Number.Natural.* m p) ⇔
    m = 0 ∨ Number.Natural.≤ n p

⊦ ∀l n.
    Byte.bit (Byte.Bits.toWord l) n ⇔
    Number.Natural.< n Byte.width ∧ Number.Natural.< n (length l) ∧ nth n l

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

⊦ (∀x. replicate 0 x = []) ∧
  ∀n x. replicate (Number.Natural.suc n) x = x :: replicate n x

⊦ ∀h1 h2 t1 t2. h1 :: t1 = h2 :: t2 ⇔ h1 = h2 ∧ t1 = t2

⊦ ∀p e.
    inverse p e ⇔
    ∀x s. parse p (Stream.append (e x) s) = Data.Option.some (x, s)

⊦ ∀l.
    Byte.Bits.fromWord (Byte.Bits.toWord l) =
    if Number.Natural.≤ (length l) Byte.width then
      l @ replicate (Number.Natural.- Byte.width (length l)) F
    else take Byte.width l

⊦ ∀l.
    Word16.Bits.fromWord (Word16.Bits.toWord l) =
    if Number.Natural.≤ (length l) Word16.width then
      l @ replicate (Number.Natural.- Word16.width (length l)) F
    else take Word16.width l

⊦ (∀m. Number.Natural.exp m 0 = 1) ∧
  ∀m n.
    Number.Natural.exp m (Number.Natural.suc n) =
    Number.Natural.* m (Number.Natural.exp m n)

⊦ (∀l. drop 0 l = l) ∧
  ∀n h t. drop (Number.Natural.suc n) (h :: t) = drop n t

⊦ (∀b f. Data.Option.case b f Data.Option.none = b) ∧
  ∀b f a. Data.Option.case b f (Data.Option.some a) = f a

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

⊦ (∀s. Stream.append [] s = s) ∧
  ∀h t s. Stream.append (h :: t) s = Stream.stream h (Stream.append t s)

⊦ ∀p s.
    parse p s = Data.Option.none ∨
    ∃b s'.
      parse p s = Data.Option.some (b, s') ∧ Stream.isProperSuffix s' s

⊦ (∀l. take 0 l = []) ∧
  ∀n h t. take (Number.Natural.suc n) (h :: t) = h :: take n t

⊦ ∀p.
    isParser p ⇔
    ∀x xs. Data.Option.case T (λ(y, xs'). Stream.isSuffix xs' xs) (p x xs)

⊦ (∀m. Number.Natural.≤ m 0 ⇔ m = 0) ∧
  ∀m n.
    Number.Natural.≤ m (Number.Natural.suc n) ⇔
    m = Number.Natural.suc n ∨ Number.Natural.≤ m n

⊦ (∀h t. nth 0 (h :: t) = h) ∧
  ∀h t n. nth (Number.Natural.suc n) (h :: t) = nth n t

⊦ ∀t. ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬t) ∧ ((t ⇔ F) ⇔ ¬t)

⊦ ∀m n q r.
    m = Number.Natural.+ (Number.Natural.* q n) r ∧ Number.Natural.< r n ⇒
    Number.Natural.div m n = q ∧ Number.Natural.mod m n = r

⊦ (∀p. parse p Stream.error = Data.Option.none) ∧
  (∀p. parse p Stream.eof = Data.Option.none) ∧
  ∀p a s. parse p (Stream.stream a s) = destParser p a s

⊦ Byte.Bits.toWord [] = Byte.fromNatural 0 ∧
  ∀h t.
    Byte.Bits.toWord (h :: t) =
    if h then
      Byte.+ (Byte.shiftLeft (Byte.Bits.toWord t) 1) (Byte.fromNatural 1)
    else Byte.shiftLeft (Byte.Bits.toWord t) 1

⊦ Word16.Bits.toWord [] = Word16.fromNatural 0 ∧
  ∀h t.
    Word16.Bits.toWord (h :: t) =
    if h then
      Word16.+ (Word16.shiftLeft (Word16.Bits.toWord t) 1)
        (Word16.fromNatural 1)
    else Word16.shiftLeft (Word16.Bits.toWord t) 1

⊦ ∀t. (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)

⊦ ∀t. (T ∨ t ⇔ T) ∧ (t ∨ T ⇔ T) ∧ (F ∨ t ⇔ t) ∧ (t ∨ F ⇔ t) ∧ (t ∨ t ⇔ t)

⊦ ∀t. (T ⇒ t ⇔ t) ∧ (t ⇒ T ⇔ T) ∧ (F ⇒ t ⇔ T) ∧ (t ⇒ t ⇔ T) ∧ (t ⇒ F ⇔ ¬t)

⊦ (∀f. zipWith f [] [] = []) ∧
  ∀f h1 h2 t1 t2.
    zipWith f (h1 :: t1) (h2 :: t2) = f h1 h2 :: zipWith f t1 t2

⊦ ∀b.
    ∃x0 x1 x2 x3 x4 x5 x6 x7.
      b =
      Byte.Bits.toWord (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: [])

⊦ ∀f p s.
    parse (partialMap f p) s =
    Data.Option.case Data.Option.none
      (λ(b, s').
         Data.Option.case Data.Option.none (λc. Data.Option.some (c, s'))
           (f b)) (parse p s)

⊦ ∀m n p.
    Number.Natural.+ m n = Number.Natural.+ n m ∧
    Number.Natural.+ (Number.Natural.+ m n) p =
    Number.Natural.+ m (Number.Natural.+ n p) ∧
    Number.Natural.+ m (Number.Natural.+ n p) =
    Number.Natural.+ n (Number.Natural.+ m p)

⊦ ∀l n.
    Byte.shiftRight (Byte.Bits.toWord l) n =
    if Number.Natural.≤ (length l) Byte.width then
      if Number.Natural.≤ (length l) n then Byte.Bits.toWord []
      else Byte.Bits.toWord (drop n l)
    else if Number.Natural.≤ Byte.width n then Byte.Bits.toWord []
    else Byte.Bits.toWord (drop n (take Byte.width l))

⊦ (∀n. Number.Natural.+ 0 n = n) ∧ (∀m. Number.Natural.+ m 0 = m) ∧
  (∀m n.
     Number.Natural.+ (Number.Natural.suc m) n =
     Number.Natural.suc (Number.Natural.+ m n)) ∧
  ∀m n.
    Number.Natural.+ m (Number.Natural.suc n) =
    Number.Natural.suc (Number.Natural.+ m n)

⊦ (∀q. Byte.Bits.compare q [] [] ⇔ q) ∧
  ∀q h1 h2 t1 t2.
    Byte.Bits.compare q (h1 :: t1) (h2 :: t2) ⇔
    Byte.Bits.compare (¬h1 ∧ h2 ∨ ¬(h1 ∧ ¬h2) ∧ q) t1 t2

⊦ (∀q. Word16.Bits.compare q [] [] ⇔ q) ∧
  ∀q h1 h2 t1 t2.
    Word16.Bits.compare q (h1 :: t1) (h2 :: t2) ⇔
    Word16.Bits.compare (¬h1 ∧ h2 ∨ ¬(h1 ∧ ¬h2) ∧ q) t1 t2

⊦ (∀e b f. Stream.case e b f Stream.error = e) ∧
  (∀e b f. Stream.case e b f Stream.eof = b) ∧
  ∀e b f a s. Stream.case e b f (Stream.stream a s) = f a s

⊦ ∀pb pc s.
    parse (parsePair pb pc) s =
    Data.Option.case Data.Option.none
      (λ(b, s').
         Data.Option.case Data.Option.none
           (λ(c, s''). Data.Option.some ((b, c), s'')) (parse pc s'))
      (parse pb s)

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

⊦ (∀n. Number.Natural.* 0 n = 0) ∧ (∀m. Number.Natural.* m 0 = 0) ∧
  (∀n. Number.Natural.* 1 n = n) ∧ (∀m. Number.Natural.* m 1 = m) ∧
  (∀m n.
     Number.Natural.* (Number.Natural.suc m) n =
     Number.Natural.+ (Number.Natural.* m n) n) ∧
  ∀m n.
    Number.Natural.* m (Number.Natural.suc n) =
    Number.Natural.+ m (Number.Natural.* m n)