| name | examples |
| version | 1.6 |
| description | All the example theories |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| show | Data.Bool |
⊦ Parser.isParser Parser.parseAll.pa
⊦ Parser.isParser Parser.parseNone.pn
⊦ Parser.isParser Data.Char.UTF8.decoder.parse
⊦ Relation.wellFounded Parser.Stream.isProperSuffix
⊦ Parser.inverse Data.Char.UTF8.decoder Data.Char.UTF8.encoder
⊦ Parser.strongInverse Data.Char.UTF8.decoder Data.Char.UTF8.encoder
⊦ ¬(Data.Byte.modulus = Number.Numeral.zero)
⊦ ¬(Data.Word16.modulus = Number.Numeral.zero)
⊦ Parser.parseAll = Parser.mkParser Parser.parseAll.pa
⊦ Parser.parseNone = Parser.mkParser Parser.parseNone.pn
⊦ Data.Char.UTF8.parseContinuationByte =
Parser.parseSome Data.Char.UTF8.isContinuationByte
⊦ Data.Char.UTF8.decoder = Parser.mkParser Data.Char.UTF8.decoder.parse
⊦ Data.Char.UTF8.decodeStream = Parser.parseStream Data.Char.UTF8.decoder
⊦ Parser.destParser Parser.parseNone = Parser.parseNone.pn
⊦ Parser.destParser Data.Char.UTF8.decoder = Data.Char.UTF8.decoder.parse
⊦ ∀w. Data.Byte.Bits.normal (Data.Byte.Bits.fromWord w)
⊦ ∀w. Data.Word16.Bits.normal (Data.Word16.Bits.fromWord w)
⊦ ∀x. Parser.Stream.isSuffix x x
⊦ ∀p. Parser.isParser (Parser.destParser p)
⊦ Data.Char.UTF8.parseTwoContinuationBytes =
Parser.parsePair Data.Char.UTF8.parseContinuationByte
Data.Char.UTF8.parseContinuationByte
⊦ Data.Char.UTF8.parseThreeContinuationBytes =
Parser.parsePair Data.Char.UTF8.parseContinuationByte
Data.Char.UTF8.parseTwoContinuationBytes
⊦ Data.Byte.toNatural (Data.Byte.Bits.toWord Data.List.[]) =
Number.Numeral.zero
⊦ Data.Word16.toNatural (Data.Word16.Bits.toWord Data.List.[]) =
Number.Numeral.zero
⊦ ∀x. Number.Natural.< (Data.Byte.toNatural x) Data.Byte.modulus
⊦ ∀p. Data.Char.isPosition p ⇔ T
⊦ ∀x. Number.Natural.< (Data.Word16.toNatural x) Data.Word16.modulus
⊦ Parser.inverse Parser.parseAll (λa. Data.List.:: a Data.List.[])
⊦ Parser.strongInverse Parser.parseAll (λa. Data.List.:: a Data.List.[])
⊦ ∀x. Data.Byte.fromNatural (Data.Byte.toNatural x) = x
⊦ ∀w. Data.Byte.Bits.toWord (Data.Byte.Bits.fromWord w) = w
⊦ ∀w. Data.List.length (Data.Byte.Bits.fromWord w) = Data.Byte.width
⊦ ∀x. Data.Word16.fromNatural (Data.Word16.toNatural x) = x
⊦ ∀w. Data.Word16.Bits.toWord (Data.Word16.Bits.fromWord w) = w
⊦ ∀w. Data.List.length (Data.Word16.Bits.fromWord w) = Data.Word16.width
⊦ ∀n.
Number.Natural.< (Number.Natural.mod n Data.Byte.modulus)
Data.Byte.modulus
⊦ ∀n.
Number.Natural.< (Number.Natural.mod n Data.Word16.modulus)
Data.Word16.modulus
⊦ ∀s. Parser.parse Parser.parseNone s = Data.Option.none
⊦ ∀pb pc. Parser.isParser (Parser.parsePair.pbc pb pc)
⊦ ∀f p. Parser.isParser (Parser.partialMap.pf f p)
⊦ Data.Byte.modulus =
Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
Data.Byte.width
⊦ Data.Byte.width =
Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)))
⊦ Data.Word16.modulus =
Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
Data.Word16.width
⊦ Parser.parse Data.Char.UTF8.decoder =
Parser.Stream.case Data.Option.none Data.Option.none
Data.Char.UTF8.decoder.parse
⊦ ∀x.
Number.Natural.div (Data.Byte.toNatural x) Data.Byte.modulus =
Number.Numeral.zero
⊦ ∀x.
Number.Natural.div (Data.Word16.toNatural x) Data.Word16.modulus =
Number.Numeral.zero
⊦ ∀l. Parser.Stream.fromList l = Parser.Stream.append l Parser.Stream.eof
⊦ ∀f. Parser.parseOption f = Parser.partialMap f Parser.parseAll
⊦ ∀a s. Parser.parseNone.pn a s = Data.Option.none
⊦ Data.Word16.width =
Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))))
⊦ ∀b.
Data.Word16.fromNatural (Data.Byte.toNatural b) =
Data.Word16.Bits.toWord (Data.Byte.Bits.fromWord b)
⊦ ∀w.
Data.Byte.fromNatural (Data.Word16.toNatural w) =
Data.Byte.Bits.toWord (Data.Word16.Bits.fromWord w)
⊦ ∀x.
Data.Byte.toNatural (Data.Byte.fromNatural x) =
Number.Natural.mod x Data.Byte.modulus
⊦ ∀x.
Data.Word16.toNatural (Data.Word16.fromNatural x) =
Number.Natural.mod x Data.Word16.modulus
⊦ ∀l. Data.Byte.Bits.normal l ⇔ Data.List.length l = Data.Byte.width
⊦ ∀l. Data.Word16.Bits.normal l ⇔ Data.List.length l = Data.Word16.width
⊦ ∀bs.
Data.Char.UTF8.decode bs =
Parser.Stream.toList
(Data.Char.UTF8.decodeStream (Parser.Stream.fromList bs))
⊦ ∀chs.
Data.Char.UTF8.encode chs =
Data.List.concat (Data.List.map Data.Char.UTF8.encoder chs)
⊦ ∀x.
Data.Byte.¬ x =
Data.Byte.fromNatural
(Number.Natural.- Data.Byte.modulus (Data.Byte.toNatural x))
⊦ ∀w.
Data.Byte.not w =
Data.Byte.Bits.toWord (Data.List.map (¬) (Data.Byte.Bits.fromWord w))
⊦ ∀w. ∃b0 b1. w = Data.Word16.fromBytes b0 b1
⊦ ∀x.
Data.Word16.¬ x =
Data.Word16.fromNatural
(Number.Natural.- Data.Word16.modulus (Data.Word16.toNatural x))
⊦ ∀w.
Data.Word16.not w =
Data.Word16.Bits.toWord
(Data.List.map (¬) (Data.Word16.Bits.fromWord w))
⊦ ∀pl. ∃b. Data.Char.isPlane b ∧ pl = Data.Char.mkPlane b
⊦ ∀pos. ∃w. Data.Char.isPosition w ∧ pos = Data.Char.mkPosition w
⊦ ∀x y. Parser.Stream.isProperSuffix x y ⇒ Parser.Stream.isSuffix x y
⊦ ∀w.
Data.Byte.Bits.fromWord w =
Data.List.map (Data.Byte.bit w)
(Data.List.interval Number.Numeral.zero Data.Byte.width)
⊦ ∀w.
Data.Word16.Bits.fromWord w =
Data.List.map (Data.Word16.bit w)
(Data.List.interval Number.Numeral.zero Data.Word16.width)
⊦ ∀n.
Number.Natural.< n Data.Byte.modulus ⇒
Number.Natural.mod n Data.Byte.modulus = n
⊦ ∀n.
Number.Natural.< n Data.Word16.modulus ⇒
Number.Natural.mod n Data.Word16.modulus = n
⊦ ∀n.
Number.Natural.mod (Number.Natural.mod n Data.Byte.modulus)
Data.Byte.modulus = Number.Natural.mod n Data.Byte.modulus
⊦ ∀n.
Number.Natural.mod (Number.Natural.mod n Data.Word16.modulus)
Data.Word16.modulus = Number.Natural.mod n Data.Word16.modulus
⊦ ∀a s. Parser.parseAll.pa a s = Data.Option.some (Data.Pair., a s)
⊦ ∀x y. Data.Byte.< x y ⇔ ¬Data.Byte.≤ y x
⊦ ∀x y. Data.Byte.- x y = Data.Byte.+ x (Data.Byte.¬ y)
⊦ ∀x y. Data.Word16.< x y ⇔ ¬Data.Word16.≤ y x
⊦ ∀x y. Data.Word16.- x y = Data.Word16.+ x (Data.Word16.¬ y)
⊦ ∀pb pc.
Parser.parsePair pb pc = Parser.mkParser (Parser.parsePair.pbc pb pc)
⊦ ∀pb pc.
Parser.destParser (Parser.parsePair pb pc) = Parser.parsePair.pbc pb pc
⊦ ∀f p. Parser.partialMap f p = Parser.mkParser (Parser.partialMap.pf f p)
⊦ ∀f p.
Parser.destParser (Parser.partialMap f p) = Parser.partialMap.pf f p
⊦ Parser.parse Parser.parseAll =
Parser.Stream.case Data.Option.none Data.Option.none
(λa s. Data.Option.some (Data.Pair., a s))
⊦ ∀l.
Number.Natural.< (Data.Byte.toNatural (Data.Byte.Bits.toWord l))
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Data.List.length l))
⊦ ∀l.
Number.Natural.< (Data.Word16.toNatural (Data.Word16.Bits.toWord l))
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Data.List.length l))
⊦ ∀l.
Data.List.length l = Data.Byte.width ⇔
Data.Byte.Bits.fromWord (Data.Byte.Bits.toWord l) = l
⊦ ∀l.
Data.List.length l = Data.Word16.width ⇔
Data.Word16.Bits.fromWord (Data.Word16.Bits.toWord l) = l
⊦ ∀x y.
Data.Byte.< x y ⇔
Number.Natural.< (Data.Byte.toNatural x) (Data.Byte.toNatural y)
⊦ ∀x y.
Data.Byte.≤ x y ⇔
Number.Natural.≤ (Data.Byte.toNatural x) (Data.Byte.toNatural y)
⊦ ∀w1 w2. Data.Byte.Bits.fromWord w1 = Data.Byte.Bits.fromWord w2 ⇔ w1 = w2
⊦ ∀x y. Data.Byte.toNatural x = Data.Byte.toNatural y ⇒ x = y
⊦ ∀w1 w2. Data.Byte.Bits.fromWord w1 = Data.Byte.Bits.fromWord w2 ⇒ w1 = w2
⊦ ∀w n.
Data.Byte.bit w n ⇔
Number.Natural.odd (Data.Byte.toNatural (Data.Byte.shiftRight w n))
⊦ ∀x y.
Data.Word16.< x y ⇔
Number.Natural.< (Data.Word16.toNatural x) (Data.Word16.toNatural y)
⊦ ∀x y.
Data.Word16.≤ x y ⇔
Number.Natural.≤ (Data.Word16.toNatural x) (Data.Word16.toNatural y)
⊦ ∀w1 w2.
Data.Word16.Bits.fromWord w1 = Data.Word16.Bits.fromWord w2 ⇔ w1 = w2
⊦ ∀x y. Data.Word16.toNatural x = Data.Word16.toNatural y ⇒ x = y
⊦ ∀w1 w2.
Data.Word16.Bits.fromWord w1 = Data.Word16.Bits.fromWord w2 ⇒ w1 = w2
⊦ ∀w n.
Data.Word16.bit w n ⇔
Number.Natural.odd (Data.Word16.toNatural (Data.Word16.shiftRight w n))
⊦ ∀x y.
Parser.Stream.isProperSuffix x y ⇒
Number.Natural.< (Parser.Stream.length x) (Parser.Stream.length y)
⊦ ∀p.
Parser.parseSome p =
Parser.parseOption
(λa. if p a then Data.Option.some a else Data.Option.none)
⊦ ∀f p. Parser.map f p = Parser.partialMap (λb. Data.Option.some (f b)) p
⊦ ∀w1 w2.
Data.Byte.Bits.compare F (Data.Byte.Bits.fromWord w1)
(Data.Byte.Bits.fromWord w2) ⇔ Data.Byte.< w1 w2
⊦ ∀w1 w2.
Data.Byte.Bits.compare T (Data.Byte.Bits.fromWord w1)
(Data.Byte.Bits.fromWord w2) ⇔ Data.Byte.≤ w1 w2
⊦ ∀b0 b1.
Data.Word16.Bits.toWord
(Data.List.@ (Data.Byte.Bits.fromWord b1)
(Data.Byte.Bits.fromWord b0)) = Data.Word16.fromBytes b0 b1
⊦ ∀w1 w2.
Data.Word16.Bits.compare F (Data.Word16.Bits.fromWord w1)
(Data.Word16.Bits.fromWord w2) ⇔ Data.Word16.< w1 w2
⊦ ∀w1 w2.
Data.Word16.Bits.compare T (Data.Word16.Bits.fromWord w1)
(Data.Word16.Bits.fromWord w2) ⇔ Data.Word16.≤ w1 w2
⊦ ∀x1 y1.
Data.Byte.fromNatural (Number.Natural.* x1 y1) =
Data.Byte.* (Data.Byte.fromNatural x1) (Data.Byte.fromNatural y1)
⊦ ∀x1 y1.
Data.Byte.fromNatural (Number.Natural.+ x1 y1) =
Data.Byte.+ (Data.Byte.fromNatural x1) (Data.Byte.fromNatural y1)
⊦ ∀x1 y1.
Data.Word16.fromNatural (Number.Natural.* x1 y1) =
Data.Word16.* (Data.Word16.fromNatural x1) (Data.Word16.fromNatural y1)
⊦ ∀x1 y1.
Data.Word16.fromNatural (Number.Natural.+ x1 y1) =
Data.Word16.+ (Data.Word16.fromNatural x1) (Data.Word16.fromNatural y1)
⊦ ∀p.
Data.Char.isPlane p ⇔
Data.Byte.< p
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))))))
⊦ ∀l.
Number.Natural.≤ Data.Byte.width (Data.List.length l) ⇒
Data.Byte.Bits.fromWord (Data.Byte.Bits.toWord l) =
Data.List.take Data.Byte.width l
⊦ ∀l.
Number.Natural.≤ Data.Word16.width (Data.List.length l) ⇒
Data.Word16.Bits.fromWord (Data.Word16.Bits.toWord l) =
Data.List.take Data.Word16.width l
⊦ ∀w1 w2.
Data.Byte.and w1 w2 =
Data.Byte.Bits.toWord
(Data.List.zipWith (∧) (Data.Byte.Bits.fromWord w1)
(Data.Byte.Bits.fromWord w2))
⊦ ∀w1 w2.
Data.Byte.or w1 w2 =
Data.Byte.Bits.toWord
(Data.List.zipWith (∨) (Data.Byte.Bits.fromWord w1)
(Data.Byte.Bits.fromWord w2))
⊦ ∀w1 w2.
Data.Word16.and w1 w2 =
Data.Word16.Bits.toWord
(Data.List.zipWith (∧) (Data.Word16.Bits.fromWord w1)
(Data.Word16.Bits.fromWord w2))
⊦ ∀w1 w2.
Data.Word16.or w1 w2 =
Data.Word16.Bits.toWord
(Data.List.zipWith (∨) (Data.Word16.Bits.fromWord w1)
(Data.Word16.Bits.fromWord w2))
⊦ ∀l n.
Data.Byte.shiftLeft (Data.Byte.Bits.toWord l) n =
Data.Byte.Bits.toWord (Data.List.@ (Data.List.replicate n F) l)
⊦ ∀l n.
Data.Word16.shiftLeft (Data.Word16.Bits.toWord l) n =
Data.Word16.Bits.toWord (Data.List.@ (Data.List.replicate n F) l)
⊦ ∀s s'.
Parser.Stream.isSuffix s s' ⇔
s = s' ∨ Parser.Stream.isProperSuffix s s'
⊦ ∀x y.
Data.Byte.toNatural (Data.Byte.+ x y) =
Number.Natural.mod
(Number.Natural.+ (Data.Byte.toNatural x) (Data.Byte.toNatural y))
Data.Byte.modulus
⊦ ∀pl.
∃b.
Data.Char.isPlane b ∧ pl = Data.Char.mkPlane b ∧
Data.Char.destPlane pl = b
⊦ ∀pos.
∃w.
Data.Char.isPosition w ∧ pos = Data.Char.mkPosition w ∧
Data.Char.destPosition pos = w
⊦ ∀x y.
Data.Word16.toNatural (Data.Word16.+ x y) =
Number.Natural.mod
(Number.Natural.+ (Data.Word16.toNatural x)
(Data.Word16.toNatural y)) Data.Word16.modulus
⊦ ∀c.
∃pl pos.
Data.Char.isChar (Data.Pair., pl pos) ∧
c = Data.Char.mkChar (Data.Pair., pl pos)
⊦ ∀n.
Data.Byte.Bits.toWord
(Data.List.:: (Number.Natural.odd n)
(Data.Byte.Bits.fromWord
(Data.Byte.fromNatural
(Number.Natural.div n
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)))))) =
Data.Byte.fromNatural n
⊦ ∀n.
Data.Word16.Bits.toWord
(Data.List.:: (Number.Natural.odd n)
(Data.Word16.Bits.fromWord
(Data.Word16.fromNatural
(Number.Natural.div n
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)))))) =
Data.Word16.fromNatural n
⊦ ∀x y z.
Parser.Stream.append (Data.List.@ x y) z =
Parser.Stream.append x (Parser.Stream.append y z)
⊦ ∀x y z.
Parser.Stream.isProperSuffix x y ∧ Parser.Stream.isProperSuffix y z ⇒
Parser.Stream.isProperSuffix x z
⊦ ∀x y z.
Parser.Stream.isSuffix x y ∧ Parser.Stream.isSuffix y z ⇒
Parser.Stream.isSuffix x z
⊦ ∀w n.
Data.Byte.bit w n ⇔
Number.Natural.odd
(Number.Natural.div (Data.Byte.toNatural w)
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
n))
⊦ ∀w n.
Data.Byte.shiftLeft w n =
Data.Byte.fromNatural
(Number.Natural.*
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
n) (Data.Byte.toNatural w))
⊦ ∀w n.
Data.Byte.shiftRight w n =
Data.Byte.fromNatural
(Number.Natural.div (Data.Byte.toNatural w)
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
n))
⊦ ∀w n.
Data.Word16.bit w n ⇔
Number.Natural.odd
(Number.Natural.div (Data.Word16.toNatural w)
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
n))
⊦ ∀w n.
Data.Word16.shiftLeft w n =
Data.Word16.fromNatural
(Number.Natural.*
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
n) (Data.Word16.toNatural w))
⊦ ∀w n.
Data.Word16.shiftRight w n =
Data.Word16.fromNatural
(Number.Natural.div (Data.Word16.toNatural w)
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
n))
⊦ ∀x y.
Data.Byte.fromNatural x = Data.Byte.fromNatural y ⇔
Number.Natural.mod x Data.Byte.modulus =
Number.Natural.mod y Data.Byte.modulus
⊦ ∀x y.
Data.Word16.fromNatural x = Data.Word16.fromNatural y ⇔
Number.Natural.mod x Data.Word16.modulus =
Number.Natural.mod y Data.Word16.modulus
⊦ ∀w.
∃b0 b1.
w = Data.Word16.fromBytes b0 b1 ∧
Data.Word16.toBytes w = Data.Pair., b0 b1
⊦ (∀a. Data.Char.mkChar (Data.Char.destChar a) = a) ∧
∀r. Data.Char.isChar r ⇔ Data.Char.destChar (Data.Char.mkChar r) = r
⊦ (∀a. Data.Char.mkPlane (Data.Char.destPlane a) = a) ∧
∀r. Data.Char.isPlane r ⇔ Data.Char.destPlane (Data.Char.mkPlane r) = r
⊦ (∀a. Data.Char.mkPosition (Data.Char.destPosition a) = a) ∧
∀r.
Data.Char.isPosition r ⇔
Data.Char.destPosition (Data.Char.mkPosition r) = r
⊦ (∀a. Parser.mkParser (Parser.destParser a) = a) ∧
∀r. Parser.isParser r ⇔ Parser.destParser (Parser.mkParser r) = r
⊦ ∀x.
x = Parser.Stream.error ∨ x = Parser.Stream.eof ∨
∃a0 a1. x = Parser.Stream.stream a0 a1
⊦ ∀p.
Parser.parse (Parser.parseSome p) =
Parser.Stream.case Data.Option.none Data.Option.none
(λa s.
if p a then Data.Option.some (Data.Pair., a s)
else Data.Option.none)
⊦ ∀m n.
Number.Natural.mod
(Number.Natural.* (Number.Natural.mod m Data.Byte.modulus)
(Number.Natural.mod n Data.Byte.modulus)) Data.Byte.modulus =
Number.Natural.mod (Number.Natural.* m n) Data.Byte.modulus
⊦ ∀m n.
Number.Natural.mod
(Number.Natural.* (Number.Natural.mod m Data.Word16.modulus)
(Number.Natural.mod n Data.Word16.modulus)) Data.Word16.modulus =
Number.Natural.mod (Number.Natural.* m n) Data.Word16.modulus
⊦ ∀m n.
Number.Natural.mod
(Number.Natural.+ (Number.Natural.mod m Data.Byte.modulus)
(Number.Natural.mod n Data.Byte.modulus)) Data.Byte.modulus =
Number.Natural.mod (Number.Natural.+ m n) Data.Byte.modulus
⊦ ∀m n.
Number.Natural.mod
(Number.Natural.+ (Number.Natural.mod m Data.Word16.modulus)
(Number.Natural.mod n Data.Word16.modulus)) Data.Word16.modulus =
Number.Natural.mod (Number.Natural.+ m n) Data.Word16.modulus
⊦ ∀f.
Parser.parse (Parser.parseOption f) =
Parser.Stream.case Data.Option.none Data.Option.none
(λa s.
Data.Option.case Data.Option.none
(λb. Data.Option.some (Data.Pair., b s)) (f a))
⊦ ∀p. (∀x. (∀y. Parser.Stream.isProperSuffix y x ⇒ p y) ⇒ p x) ⇒ ∀x. p x
⊦ ∀b.
Data.Char.UTF8.isContinuationByte b ⇔
Data.Byte.bit b
(Number.Numeral.bit1
(Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero))) ∧
¬Data.Byte.bit b
(Number.Numeral.bit0
(Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero)))
⊦ ∀l.
Number.Natural.≤ (Data.List.length l) Data.Byte.width ⇒
Data.Byte.Bits.fromWord (Data.Byte.Bits.toWord l) =
Data.List.@ l
(Data.List.replicate
(Number.Natural.- Data.Byte.width (Data.List.length l)) F)
⊦ ∀l.
Number.Natural.≤ (Data.List.length l) Data.Word16.width ⇒
Data.Word16.Bits.fromWord (Data.Word16.Bits.toWord l) =
Data.List.@ l
(Data.List.replicate
(Number.Natural.- Data.Word16.width (Data.List.length l)) F)
⊦ ∀p a s.
Parser.destParser (Parser.parseSome p) a s =
if p a then Data.Option.some (Data.Pair., a s) else Data.Option.none
⊦ ∀f a s.
Parser.destParser (Parser.parseOption f) a s =
Data.Option.case Data.Option.none
(λb. Data.Option.some (Data.Pair., b s)) (f a)
⊦ ∀f e.
(∀b. f (e b) = Data.Option.some b) ⇒
Parser.inverse (Parser.parseOption f)
(λb. Data.List.:: (e b) Data.List.[])
⊦ ∀q w1 w2.
Data.Byte.Bits.compare q (Data.Byte.Bits.fromWord w1)
(Data.Byte.Bits.fromWord w2) ⇔
if q then Data.Byte.≤ w1 w2 else Data.Byte.< w1 w2
⊦ ∀q w1 w2.
Data.Word16.Bits.compare q (Data.Word16.Bits.fromWord w1)
(Data.Word16.Bits.fromWord w2) ⇔
if q then Data.Word16.≤ w1 w2 else Data.Word16.< w1 w2
⊦ ∀w1 w2.
(∀i.
Number.Natural.< i Data.Byte.width ⇒
(Data.Byte.bit w1 i ⇔ Data.Byte.bit w2 i)) ⇒ w1 = w2
⊦ ∀w1 w2.
(∀i.
Number.Natural.< i Data.Word16.width ⇒
(Data.Word16.bit w1 i ⇔ Data.Word16.bit w2 i)) ⇒ w1 = w2
⊦ ∀l.
Number.Natural.<
(Number.Natural.+
(Number.Natural.*
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Data.Byte.toNatural (Data.Byte.Bits.toWord l)))
(Number.Numeral.bit1 Number.Numeral.zero))
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Number.Natural.suc (Data.List.length l)))
⊦ ∀l.
Number.Natural.<
(Number.Natural.+
(Number.Natural.*
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Data.Word16.toNatural (Data.Word16.Bits.toWord l)))
(Number.Numeral.bit1 Number.Numeral.zero))
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Number.Natural.suc (Data.List.length l)))
⊦ ∀b1 b2.
Data.Word16.fromBytes b1 b2 =
Data.Word16.or
(Data.Word16.shiftLeft
(Data.Word16.fromNatural (Data.Byte.toNatural b1))
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)))))
(Data.Word16.fromNatural (Data.Byte.toNatural b2))
⊦ ∀x y.
Number.Natural.< x Data.Byte.modulus ∧
Number.Natural.< y Data.Byte.modulus ∧
Data.Byte.fromNatural x = Data.Byte.fromNatural y ⇒ x = y
⊦ ∀x y.
Number.Natural.< x Data.Word16.modulus ∧
Number.Natural.< y Data.Word16.modulus ∧
Data.Word16.fromNatural x = Data.Word16.fromNatural y ⇒ x = y
⊦ ∀l n.
Data.Byte.bit (Data.Byte.Bits.toWord l) n ⇔
Number.Natural.< n Data.Byte.width ∧
Number.Natural.< n (Data.List.length l) ∧ Data.List.nth n l
⊦ ∀l n.
Data.Word16.bit (Data.Word16.Bits.toWord l) n ⇔
Number.Natural.< n Data.Word16.width ∧
Number.Natural.< n (Data.List.length l) ∧ Data.List.nth n l
⊦ ∀n.
Data.Byte.fromNatural n =
Data.Byte.Bits.toWord
(if n = Number.Numeral.zero then Data.List.[]
else
Data.List.:: (Number.Natural.odd n)
(Data.Byte.Bits.fromWord
(Data.Byte.fromNatural
(Number.Natural.div n
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))))))
⊦ ∀n.
Data.Word16.fromNatural n =
Data.Word16.Bits.toWord
(if n = Number.Numeral.zero then Data.List.[]
else
Data.List.:: (Number.Natural.odd n)
(Data.Word16.Bits.fromWord
(Data.Word16.fromNatural
(Number.Natural.div n
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))))))
⊦ ∀p a s b s'.
Parser.destParser p a s = Data.Option.some (Data.Pair., b s') ⇒
Parser.Stream.isSuffix s' s
⊦ ∀a0 a1 a0' a1'.
Parser.Stream.stream a0 a1 = Parser.Stream.stream a0' a1' ⇔
a0 = a0' ∧ a1 = a1'
⊦ ∀p e.
Parser.inverse p e ⇔
∀x s.
Parser.parse p (Parser.Stream.append (e x) s) =
Data.Option.some (Data.Pair., x s)
⊦ Parser.Stream.length Parser.Stream.error = Number.Numeral.zero ∧
Parser.Stream.length Parser.Stream.eof = Number.Numeral.zero ∧
∀a s.
Parser.Stream.length (Parser.Stream.stream a s) =
Number.Natural.suc (Parser.Stream.length s)
⊦ ∀l.
Data.Byte.Bits.fromWord (Data.Byte.Bits.toWord l) =
if Number.Natural.≤ (Data.List.length l) Data.Byte.width then
Data.List.@ l
(Data.List.replicate
(Number.Natural.- Data.Byte.width (Data.List.length l)) F)
else Data.List.take Data.Byte.width l
⊦ ∀l.
Data.Word16.Bits.fromWord (Data.Word16.Bits.toWord l) =
if Number.Natural.≤ (Data.List.length l) Data.Word16.width then
Data.List.@ l
(Data.List.replicate
(Number.Natural.- Data.Word16.width (Data.List.length l)) F)
else Data.List.take Data.Word16.width l
⊦ ∀P.
P Parser.Stream.error ∧ P Parser.Stream.eof ∧
(∀a0 a1. P a1 ⇒ P (Parser.Stream.stream a0 a1)) ⇒ ∀x. P x
⊦ ∀c.
∃pl pos.
Data.Char.isChar (Data.Pair., pl pos) ∧
c = Data.Char.mkChar (Data.Pair., pl pos) ∧
Data.Char.destChar c = Data.Pair., pl pos
⊦ (∀s. Parser.Stream.append Data.List.[] s = s) ∧
∀h t s.
Parser.Stream.append (Data.List.:: h t) s =
Parser.Stream.stream h (Parser.Stream.append t s)
⊦ ∀w.
Data.Pair.,
(Data.Byte.Bits.toWord
(Data.List.drop
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))))
(Data.Word16.Bits.fromWord w)))
(Data.Byte.Bits.toWord
(Data.List.take
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))))
(Data.Word16.Bits.fromWord w))) = Data.Word16.toBytes w
⊦ ∀h t.
Data.Byte.toNatural (Data.Byte.Bits.toWord (Data.List.:: h t)) =
Number.Natural.mod
(Number.Natural.+
(Number.Natural.*
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Data.Byte.toNatural (Data.Byte.Bits.toWord t)))
(if h then Number.Numeral.bit1 Number.Numeral.zero
else Number.Numeral.zero)) Data.Byte.modulus
⊦ ∀h t.
Data.Word16.toNatural (Data.Word16.Bits.toWord (Data.List.:: h t)) =
Number.Natural.mod
(Number.Natural.+
(Number.Natural.*
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Data.Word16.toNatural (Data.Word16.Bits.toWord t)))
(if h then Number.Numeral.bit1 Number.Numeral.zero
else Number.Numeral.zero)) Data.Word16.modulus
⊦ ∀h t.
Number.Natural.<
(Number.Natural.+
(Number.Natural.*
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Data.Byte.toNatural (Data.Byte.Bits.toWord t)))
(if h then Number.Numeral.bit1 Number.Numeral.zero
else Number.Numeral.zero))
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Number.Natural.suc (Data.List.length t)))
⊦ ∀h t.
Number.Natural.<
(Number.Natural.+
(Number.Natural.*
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Data.Word16.toNatural (Data.Word16.Bits.toWord t)))
(if h then Number.Numeral.bit1 Number.Numeral.zero
else Number.Numeral.zero))
(Number.Natural.exp
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
(Number.Natural.suc (Data.List.length t)))
⊦ ∀l n.
Number.Natural.≤ (Data.List.length l) Data.Byte.width ⇒
Data.Byte.shiftRight (Data.Byte.Bits.toWord l) n =
if Number.Natural.≤ (Data.List.length l) n then
Data.Byte.Bits.toWord Data.List.[]
else Data.Byte.Bits.toWord (Data.List.drop n l)
⊦ ∀l n.
Number.Natural.≤ (Data.List.length l) Data.Word16.width ⇒
Data.Word16.shiftRight (Data.Word16.Bits.toWord l) n =
if Number.Natural.≤ (Data.List.length l) n then
Data.Word16.Bits.toWord Data.List.[]
else Data.Word16.Bits.toWord (Data.List.drop n l)
⊦ ∀p s.
Parser.parse p s = Data.Option.none ∨
∃b s'.
Parser.parse p s = Data.Option.some (Data.Pair., b s') ∧
Parser.Stream.isProperSuffix s' s
⊦ ¬(Parser.Stream.error = Parser.Stream.eof) ∧
(∀a0' a1'. ¬(Parser.Stream.error = Parser.Stream.stream a0' a1')) ∧
∀a0' a1'. ¬(Parser.Stream.eof = Parser.Stream.stream a0' a1')
⊦ ∀l n.
Number.Natural.≤ Data.Byte.width (Data.List.length l) ⇒
Data.Byte.shiftRight (Data.Byte.Bits.toWord l) n =
if Number.Natural.≤ Data.Byte.width n then
Data.Byte.Bits.toWord Data.List.[]
else
Data.Byte.Bits.toWord
(Data.List.drop n (Data.List.take Data.Byte.width l))
⊦ ∀l n.
Number.Natural.≤ Data.Word16.width (Data.List.length l) ⇒
Data.Word16.shiftRight (Data.Word16.Bits.toWord l) n =
if Number.Natural.≤ Data.Word16.width n then
Data.Word16.Bits.toWord Data.List.[]
else
Data.Word16.Bits.toWord
(Data.List.drop n (Data.List.take Data.Word16.width l))
⊦ ∀f p g e.
Parser.inverse p e ∧ (∀b. f (g b) = b) ⇒
Parser.inverse (Parser.map f p) (λc. e (g c))
⊦ ∀p.
Parser.isParser p ⇔
∀x xs.
Data.Option.case T
(λ(Data.Pair., y xs'). Parser.Stream.isSuffix xs' xs) (p x xs)
⊦ ∀f p g e.
Parser.inverse p e ∧ (∀b. f (g b) = Data.Option.some b) ⇒
Parser.inverse (Parser.partialMap f p) (λc. e (g c))
⊦ ∀p a s.
Parser.destParser p a s = Data.Option.none ∨
∃b s'.
Parser.destParser p a s = Data.Option.some (Data.Pair., b s') ∧
Parser.Stream.isSuffix s' s
⊦ Parser.Stream.toList Parser.Stream.error = Data.Option.none ∧
Parser.Stream.toList Parser.Stream.eof = Data.Option.some Data.List.[] ∧
∀a s.
Parser.Stream.toList (Parser.Stream.stream a s) =
Data.Option.case Data.Option.none
(λl. Data.Option.some (Data.List.:: a l)) (Parser.Stream.toList s)
⊦ ∀w.
Data.Word16.toBytes w =
Data.Pair.,
(Data.Byte.fromNatural
(Data.Word16.toNatural
(Data.Word16.shiftRight w
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)))))))
(Data.Byte.fromNatural
(Data.Word16.toNatural
(Data.Word16.and w
(Data.Word16.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))))))
⊦ ∀p a s.
Parser.isParser p ⇒
p a s = Data.Option.none ∨
∃b s'.
p a s = Data.Option.some (Data.Pair., b s') ∧
Parser.Stream.isSuffix s' s
⊦ ∀f0 f1 f2.
∃fn.
fn Parser.Stream.error = f0 ∧ fn Parser.Stream.eof = f1 ∧
∀a0 a1. fn (Parser.Stream.stream a0 a1) = f2 a0 a1 (fn a1)
⊦ (∀p. Parser.parse p Parser.Stream.error = Data.Option.none) ∧
(∀p. Parser.parse p Parser.Stream.eof = Data.Option.none) ∧
∀p a s.
Parser.parse p (Parser.Stream.stream a s) = Parser.destParser p a s
⊦ ∀f p s.
Parser.parse (Parser.map f p) s =
Data.Option.case Data.Option.none
(λ(Data.Pair., b s'). Data.Option.some (Data.Pair., (f b) s'))
(Parser.parse p s)
⊦ Data.Byte.Bits.toWord Data.List.[] =
Data.Byte.fromNatural Number.Numeral.zero ∧
∀h t.
Data.Byte.Bits.toWord (Data.List.:: h t) =
if h then
Data.Byte.+
(Data.Byte.shiftLeft (Data.Byte.Bits.toWord t)
(Number.Numeral.bit1 Number.Numeral.zero))
(Data.Byte.fromNatural (Number.Numeral.bit1 Number.Numeral.zero))
else
Data.Byte.shiftLeft (Data.Byte.Bits.toWord t)
(Number.Numeral.bit1 Number.Numeral.zero)
⊦ Data.Word16.Bits.toWord Data.List.[] =
Data.Word16.fromNatural Number.Numeral.zero ∧
∀h t.
Data.Word16.Bits.toWord (Data.List.:: h t) =
if h then
Data.Word16.+
(Data.Word16.shiftLeft (Data.Word16.Bits.toWord t)
(Number.Numeral.bit1 Number.Numeral.zero))
(Data.Word16.fromNatural (Number.Numeral.bit1 Number.Numeral.zero))
else
Data.Word16.shiftLeft (Data.Word16.Bits.toWord t)
(Number.Numeral.bit1 Number.Numeral.zero)
⊦ ∀p e.
Parser.strongInverse p e ⇔
Parser.inverse p e ∧
∀s x s'.
Parser.parse p s = Data.Option.some (Data.Pair., x s') ⇒
s = Parser.Stream.append (e x) s'
⊦ ∀pb pc eb ec.
Parser.inverse pb eb ∧ Parser.inverse pc ec ⇒
Parser.inverse (Parser.parsePair pb pc)
(λ(Data.Pair., b c). Data.List.@ (eb b) (ec c))
⊦ ∀pb pc eb ec.
Parser.strongInverse pb eb ∧ Parser.strongInverse pc ec ⇒
Parser.strongInverse (Parser.parsePair pb pc)
(λ(Data.Pair., b c). Data.List.@ (eb b) (ec c))
⊦ (∀s. Parser.Stream.isProperSuffix s Parser.Stream.error ⇔ F) ∧
(∀s. Parser.Stream.isProperSuffix s Parser.Stream.eof ⇔ F) ∧
∀s a s'.
Parser.Stream.isProperSuffix s (Parser.Stream.stream a s') ⇔
s = s' ∨ Parser.Stream.isProperSuffix s s'
⊦ ∀b.
∃x0 x1 x2 x3 x4 x5 x6 x7.
b =
Data.Byte.Bits.toWord
(Data.List.:: x0
(Data.List.:: x1
(Data.List.:: x2
(Data.List.:: x3
(Data.List.:: x4
(Data.List.:: x5
(Data.List.:: x6
(Data.List.:: x7 Data.List.[]))))))))
⊦ ∀f p a s.
Parser.destParser (Parser.map f p) a s =
Data.Option.case Data.Option.none
(λ(Data.Pair., b s'). Data.Option.some (Data.Pair., (f b) s'))
(Parser.destParser p a s)
⊦ ∀f p s.
Parser.parse (Parser.partialMap f p) s =
Data.Option.case Data.Option.none
(λ(Data.Pair., b s').
Data.Option.case Data.Option.none
(λc. Data.Option.some (Data.Pair., c s')) (f b))
(Parser.parse p s)
⊦ ∀h.
(∀f g s.
(∀s'. Parser.Stream.isProperSuffix s' s ⇒ f s' = g s') ⇒
h f s = h g s) ⇒ ∃f. ∀s. f s = h f s
⊦ ∀l n.
Data.Byte.shiftRight (Data.Byte.Bits.toWord l) n =
if Number.Natural.≤ (Data.List.length l) Data.Byte.width then
if Number.Natural.≤ (Data.List.length l) n then
Data.Byte.Bits.toWord Data.List.[]
else Data.Byte.Bits.toWord (Data.List.drop n l)
else if Number.Natural.≤ Data.Byte.width n then
Data.Byte.Bits.toWord Data.List.[]
else
Data.Byte.Bits.toWord
(Data.List.drop n (Data.List.take Data.Byte.width l))
⊦ ∀l n.
Data.Word16.shiftRight (Data.Word16.Bits.toWord l) n =
if Number.Natural.≤ (Data.List.length l) Data.Word16.width then
if Number.Natural.≤ (Data.List.length l) n then
Data.Word16.Bits.toWord Data.List.[]
else Data.Word16.Bits.toWord (Data.List.drop n l)
else if Number.Natural.≤ Data.Word16.width n then
Data.Word16.Bits.toWord Data.List.[]
else
Data.Word16.Bits.toWord
(Data.List.drop n (Data.List.take Data.Word16.width l))
⊦ ∀f p a s.
Parser.partialMap.pf f p a s =
Data.Option.case Data.Option.none
(λ(Data.Pair., b s').
Data.Option.case Data.Option.none
(λc. Data.Option.some (Data.Pair., c s')) (f b))
(Parser.destParser p a s)
⊦ ∀f e.
(∀b. f (e b) = Data.Option.some b) ∧
(∀a1 a2 b.
f a1 = Data.Option.some b ∧ f a2 = Data.Option.some b ⇒ a1 = a2) ⇒
Parser.strongInverse (Parser.parseOption f)
(λb. Data.List.:: (e b) Data.List.[])
⊦ (∀q. Data.Byte.Bits.compare q Data.List.[] Data.List.[] ⇔ q) ∧
∀q h1 h2 t1 t2.
Data.Byte.Bits.compare q (Data.List.:: h1 t1) (Data.List.:: h2 t2) ⇔
Data.Byte.Bits.compare (¬h1 ∧ h2 ∨ ¬(h1 ∧ ¬h2) ∧ q) t1 t2
⊦ (∀q. Data.Word16.Bits.compare q Data.List.[] Data.List.[] ⇔ q) ∧
∀q h1 h2 t1 t2.
Data.Word16.Bits.compare q (Data.List.:: h1 t1) (Data.List.:: h2 t2) ⇔
Data.Word16.Bits.compare (¬h1 ∧ h2 ∨ ¬(h1 ∧ ¬h2) ∧ q) t1 t2
⊦ ∀p.
Parser.parseStream p Parser.Stream.error = Parser.Stream.error ∧
Parser.parseStream p Parser.Stream.eof = Parser.Stream.eof ∧
∀a s.
Parser.parseStream p (Parser.Stream.stream a s) =
Data.Option.case Parser.Stream.error
(λ(Data.Pair., b s').
Parser.Stream.stream b (Parser.parseStream p s'))
(Parser.destParser p a s)
⊦ ∀f p g e.
Parser.strongInverse p e ∧ (∀b. f (g b) = b) ∧
(∀b1 b2 c. f b1 = c ∧ f b2 = c ⇒ b1 = b2) ⇒
Parser.strongInverse (Parser.map f p) (λc. e (g c))
⊦ (∀e b f. Parser.Stream.case e b f Parser.Stream.error = e) ∧
(∀e b f. Parser.Stream.case e b f Parser.Stream.eof = b) ∧
∀e b f a s. Parser.Stream.case e b f (Parser.Stream.stream a s) = f a s
⊦ ∀pb pc s.
Parser.parse (Parser.parsePair pb pc) s =
Data.Option.case Data.Option.none
(λ(Data.Pair., b s').
Data.Option.case Data.Option.none
(λ(Data.Pair., c s'').
Data.Option.some (Data.Pair., (Data.Pair., b c) s''))
(Parser.parse pc s')) (Parser.parse pb s)
⊦ ∀f p g e.
Parser.strongInverse p e ∧ (∀b. f (g b) = Data.Option.some b) ∧
(∀b1 b2 c.
f b1 = Data.Option.some c ∧ f b2 = Data.Option.some c ⇒ b1 = b2) ⇒
Parser.strongInverse (Parser.partialMap f p) (λc. e (g c))
⊦ ∀pb pc a s.
Parser.parsePair.pbc pb pc a s =
Data.Option.case Data.Option.none
(λ(Data.Pair., b s').
Data.Option.case Data.Option.none
(λ(Data.Pair., c s'').
Data.Option.some (Data.Pair., (Data.Pair., b c) s''))
(Parser.parse pc s')) (Parser.destParser pb a s)
⊦ ∀w.
∃x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15.
w =
Data.Word16.Bits.toWord
(Data.List.:: x0
(Data.List.:: x1
(Data.List.:: x2
(Data.List.:: x3
(Data.List.:: x4
(Data.List.:: x5
(Data.List.:: x6
(Data.List.:: x7
(Data.List.:: x8
(Data.List.:: x9
(Data.List.:: x10
(Data.List.:: x11
(Data.List.:: x12
(Data.List.:: x13
(Data.List.:: x14
(Data.List.:: x15
Data.List.[]))))))))))))))))
⊦ ∀p0 p1.
Data.Char.UTF8.encoder.encode1 p0 p1 =
let b00 =
Data.Byte.shiftLeft p0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)) in
let b01 =
Data.Byte.shiftRight
(Data.Byte.and p1
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))))
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))) in
let b0 =
Data.Byte.or
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero)))))))))
(Data.Byte.or b00 b01) in
let b10 =
Data.Byte.and p1
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))) in
let b1 =
Data.Byte.or
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
Number.Numeral.zero))))))))) b10 in
Data.List.:: b0 (Data.List.:: b1 Data.List.[])
⊦ ∀ch.
Data.Char.UTF8.encoder ch =
let (Data.Pair., pl pos) = Data.Char.destChar ch in
let p = Data.Char.destPlane pl in
let (Data.Pair., p0 p1) =
Data.Word16.toBytes (Data.Char.destPosition pos) in
if p = Data.Byte.fromNatural Number.Numeral.zero then
if p0 = Data.Byte.fromNatural Number.Numeral.zero ∧
¬Data.Byte.bit p1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero)))
then Data.List.:: p1 Data.List.[]
else if Data.Byte.and
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero)))))))))
p0 = Data.Byte.fromNatural Number.Numeral.zero
then Data.Char.UTF8.encoder.encode1 p0 p1
else Data.Char.UTF8.encoder.encode2 p0 p1
else Data.Char.UTF8.encoder.encode3 p p0 p1
⊦ ∀b0 s.
Data.Char.UTF8.decoder.parse b0 s =
if Data.Byte.bit b0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero)))
then
if Data.Byte.bit b0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero)))
then
if Data.Byte.bit b0
(Number.Numeral.bit1
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)))
then
if Data.Byte.bit b0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)))
then
if Data.Byte.bit b0
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))
then Data.Option.none
else
Parser.parse
(Parser.partialMap (Data.Char.UTF8.decoder.decode3 b0)
Data.Char.UTF8.parseThreeContinuationBytes) s
else
Parser.parse
(Parser.partialMap (Data.Char.UTF8.decoder.decode2 b0)
Data.Char.UTF8.parseTwoContinuationBytes) s
else
Parser.parse
(Parser.partialMap (Data.Char.UTF8.decoder.decode1 b0)
Data.Char.UTF8.parseContinuationByte) s
else Data.Option.none
else
let pl =
Data.Char.mkPlane (Data.Byte.fromNatural Number.Numeral.zero) in
let pos =
Data.Char.mkPosition
(Data.Word16.fromBytes
(Data.Byte.fromNatural Number.Numeral.zero) b0) in
let ch = Data.Char.mkChar (Data.Pair., pl pos) in
Data.Option.some (Data.Pair., ch s)
⊦ ∀pl pos.
Data.Char.isChar (Data.Pair., pl pos) ⇔
let pli = Data.Char.destPlane pl in
let posi = Data.Char.destPosition pos in
¬(pli = Data.Byte.fromNatural Number.Numeral.zero) ∨
Data.Word16.< posi
(Data.Word16.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))))))))))) ∨
Data.Word16.<
(Data.Word16.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero)))))))))))))))))
posi ∧
Data.Word16.< posi
(Data.Word16.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero)))))))))))))))))
⊦ ∀b0 b1.
Data.Char.UTF8.decoder.decode1 b0 b1 =
let pl =
Data.Char.mkPlane (Data.Byte.fromNatural Number.Numeral.zero) in
let p0 =
Data.Byte.shiftRight
(Data.Byte.and b0
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero)))))))
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)) in
let y1 =
Data.Byte.shiftLeft
(Data.Byte.and b0
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))))
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))) in
let x1 =
Data.Byte.and b1
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))) in
let p1 = Data.Byte.or y1 x1 in
if p0 = Data.Byte.fromNatural Number.Numeral.zero ∧
Data.Byte.< p1
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
Number.Numeral.zero)))))))))
then Data.Option.none
else
let pos = Data.Char.mkPosition (Data.Word16.fromBytes p0 p1) in
let ch = Data.Char.mkChar (Data.Pair., pl pos) in
Data.Option.some ch
⊦ ∀p0 p1.
Data.Char.UTF8.encoder.encode2 p0 p1 =
let b00 =
Data.Byte.shiftRight
(Data.Byte.and p0
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))))
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))) in
let b0 =
Data.Byte.or
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))) b00 in
let b10 =
Data.Byte.shiftLeft
(Data.Byte.and p0
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))))))
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)) in
let b11 =
Data.Byte.shiftRight
(Data.Byte.and p1
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))))
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))) in
let b1 =
Data.Byte.or
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
Number.Numeral.zero)))))))))
(Data.Byte.or b10 b11) in
let b20 =
Data.Byte.and p1
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))) in
let b2 =
Data.Byte.or
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
Number.Numeral.zero))))))))) b20 in
Data.List.:: b0 (Data.List.:: b1 (Data.List.:: b2 Data.List.[]))
⊦ ∀b0 b1 b2 b3.
Data.Char.UTF8.decoder.decode3 b0
(Data.Pair., b1 (Data.Pair., b2 b3)) =
let w =
Data.Byte.shiftLeft
(Data.Byte.and b0
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero)))))
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)) in
let z =
Data.Byte.shiftRight
(Data.Byte.and b1
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))) in
let p = Data.Byte.or w z in
if p = Data.Byte.fromNatural Number.Numeral.zero ∨
Data.Byte.<
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)))))) p
then Data.Option.none
else
let pl = Data.Char.mkPlane p in
let z0 =
Data.Byte.shiftLeft
(Data.Byte.and b1
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))))))
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))) in
let y0 =
Data.Byte.shiftRight
(Data.Byte.and b2
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)) in
let p0 = Data.Byte.or z0 y0 in
let y1 =
Data.Byte.shiftLeft
(Data.Byte.and b2
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))))
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))) in
let x1 =
Data.Byte.and b3
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))) in
let p1 = Data.Byte.or y1 x1 in
let pos = Data.Char.mkPosition (Data.Word16.fromBytes p0 p1) in
let ch = Data.Char.mkChar (Data.Pair., pl pos) in
Data.Option.some ch
⊦ ∀b0 b1 b2.
Data.Char.UTF8.decoder.decode2 b0 (Data.Pair., b1 b2) =
let z0 =
Data.Byte.shiftLeft
(Data.Byte.and b0
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))))))
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))) in
let y0 =
Data.Byte.shiftRight
(Data.Byte.and b1
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)) in
let p0 = Data.Byte.or z0 y0 in
if Data.Byte.< p0
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))))) ∨
Data.Byte.≤
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))) p0 ∧
Data.Byte.≤ p0
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero)))))))))
then Data.Option.none
else
let y1 =
Data.Byte.shiftLeft
(Data.Byte.and b1
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))))
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))) in
let x1 =
Data.Byte.and b2
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))) in
let p1 = Data.Byte.or y1 x1 in
if p0 =
Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero)))))))) ∧
Data.Byte.≤
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))) p1
then Data.Option.none
else
let pl =
Data.Char.mkPlane
(Data.Byte.fromNatural Number.Numeral.zero) in
let pos = Data.Char.mkPosition (Data.Word16.fromBytes p0 p1) in
let ch = Data.Char.mkChar (Data.Pair., pl pos) in
Data.Option.some ch
⊦ ∀p p0 p1.
Data.Char.UTF8.encoder.encode3 p p0 p1 =
let b00 =
Data.Byte.shiftRight
(Data.Byte.and p
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero)))))))
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)) in
let b0 =
Data.Byte.or
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))) b00 in
let b10 =
Data.Byte.shiftLeft
(Data.Byte.and p
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))))
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))) in
let b11 =
Data.Byte.shiftRight
(Data.Byte.and p0
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))))
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero))) in
let b1 =
Data.Byte.or
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
Number.Numeral.zero)))))))))
(Data.Byte.or b10 b11) in
let b20 =
Data.Byte.shiftLeft
(Data.Byte.and p0
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))))))
(Number.Numeral.bit0
(Number.Numeral.bit1 Number.Numeral.zero)) in
let b21 =
Data.Byte.shiftRight
(Data.Byte.and p1
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))))))
(Number.Numeral.bit0
(Number.Numeral.bit1
(Number.Numeral.bit1 Number.Numeral.zero))) in
let b2 =
Data.Byte.or
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
Number.Numeral.zero)))))))))
(Data.Byte.or b20 b21) in
let b30 =
Data.Byte.and p1
(Data.Byte.fromNatural
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
(Number.Numeral.bit1
Number.Numeral.zero))))))) in
let b3 =
Data.Byte.or
(Data.Byte.fromNatural
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit0
(Number.Numeral.bit1
Number.Numeral.zero))))))))) b30 in
Data.List.:: b0
(Data.List.:: b1 (Data.List.:: b2 (Data.List.:: b3 Data.List.[])))
⊦ T
⊦ ∀x. x = x
⊦ ∀n. Number.Natural.≤ Number.Numeral.zero n
⊦ ∀n. Number.Natural.≤ n n
⊦ ∀m. Relation.wellFounded (Relation.measure m)
⊦ F ⇔ ∀p. p
⊦ let = λf x. f x
⊦ ∀x. Function.id x = x
⊦ ∀t. t ∨ ¬t
⊦ ∀n. Number.Natural.< Number.Numeral.zero (Number.Natural.suc n)
⊦ (¬) = λp. p ⇒ F
⊦ (∃) = λP. P ((select) P)
⊦ ∀a. ∃x. x = a
⊦ ∀a. ∃!x. x = a
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀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 = Number.Numeral.zero)
⊦ ∀n. Number.Natural.even n ∨ Number.Natural.odd n
⊦ ∀m. Number.Natural.+ m Number.Numeral.zero = m
⊦ ∀n. Number.Natural.- n n = Number.Numeral.zero
⊦ ∀n.
Number.Natural.even
(Number.Natural.*
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)) n)
⊦ ∀n. Number.Numeral.bit0 n = Number.Natural.+ n n
⊦ ∀n. ¬Number.Natural.even n ⇔ Number.Natural.odd n
⊦ ∀n. ¬Number.Natural.odd n ⇔ Number.Natural.even n
⊦ ∀n. Number.Natural.div n (Number.Numeral.bit1 Number.Numeral.zero) = n
⊦ ∀n. Number.Natural.exp n (Number.Numeral.bit1 Number.Numeral.zero) = n
⊦ ∀n.
Number.Natural.mod n (Number.Numeral.bit1 Number.Numeral.zero) =
Number.Numeral.zero
⊦ ∀l. Data.List.take (Data.List.length l) l = l
⊦ ∀x. (select y. y = x) = x
⊦ ∀m n. Number.Natural.≤ m (Number.Natural.+ m n)
⊦ ∀m n. Number.Natural.≤ n (Number.Natural.+ m n)
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)
⊦ ∀n.
Number.Natural.odd
(Number.Natural.suc
(Number.Natural.*
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
n))
⊦ ∀m.
Number.Natural.suc m =
Number.Natural.+ m (Number.Numeral.bit1 Number.Numeral.zero)
⊦ ∀n. Number.Numeral.bit1 n = Number.Natural.suc (Number.Natural.+ n n)
⊦ ∀x. Data.Pair., (Data.Pair.fst x) (Data.Pair.snd x) = x
⊦ ∀x y. Data.Pair.fst (Data.Pair., x y) = x
⊦ ∀x y. Data.Pair.snd (Data.Pair., x y) = y
⊦ ∀h t. Data.List.tail (Data.List.:: h t) = t
⊦ ∀n x. Data.List.length (Data.List.replicate n x) = n
⊦ ∀m n. Data.List.length (Data.List.interval m n) = n
⊦ ∀t h. Data.List.head (Data.List.:: h t) = h
⊦ ∀P x. P x ⇒ P ((select) P)
⊦ (¬T ⇔ F) ∧ (¬F ⇔ T)
⊦ ∀n. Number.Natural.< Number.Numeral.zero n ⇔ ¬(n = Number.Numeral.zero)
⊦ ∀l. Data.List.length l = Number.Numeral.zero ⇔ l = Data.List.[]
⊦ ∀f y. (λx. f x) y = f y
⊦ ∀p. ∃x y. p = Data.Pair., x y
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀x y. x = y ⇒ y = x
⊦ ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1
⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1
⊦ ∀a b. (a ⇔ b) ⇒ a ⇒ b
⊦ ∀m n. Number.Natural.* m n = Number.Natural.* n m
⊦ ∀m n. m = n ⇒ Number.Natural.≤ m n
⊦ ∀m n. Number.Natural.< m n ⇒ Number.Natural.≤ m n
⊦ ∀m n. Number.Natural.< m n ∨ Number.Natural.≤ n m
⊦ ∀m n. Number.Natural.≤ m n ∨ Number.Natural.≤ n m
⊦ ∀m n. Number.Natural.- m (Number.Natural.+ m n) = Number.Numeral.zero
⊦ ∀m n. Number.Natural.- (Number.Natural.+ m n) m = n
⊦ ∀m n. Number.Natural.- (Number.Natural.+ m n) n = m
⊦ ∀l f. Data.List.length (Data.List.map f l) = Data.List.length l
⊦ ∀n.
Number.Natural.*
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)) n =
Number.Natural.+ n n
⊦ ∀m. Relation.measure m = λx y. Number.Natural.< (m x) (m y)
⊦ ∀m n. ¬(Number.Natural.< m n ∧ Number.Natural.≤ n m)
⊦ ∀m n. ¬(Number.Natural.≤ m n ∧ Number.Natural.< n m)
⊦ ∀m n. ¬Number.Natural.< m n ⇔ Number.Natural.≤ n m
⊦ ∀m n. ¬Number.Natural.≤ m n ⇔ Number.Natural.< n m
⊦ ∀m n. Number.Natural.< m (Number.Natural.suc n) ⇔ Number.Natural.≤ m n
⊦ ∀m n. Number.Natural.≤ (Number.Natural.suc m) n ⇔ Number.Natural.< m n
⊦ ∀m. m = Number.Numeral.zero ∨ ∃n. m = Number.Natural.suc n
⊦ ∀x. x = Data.Option.none ∨ ∃a. x = Data.Option.some a
⊦ ∀P. (∀b. P b) ⇔ P T ∧ P F
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ ∀n.
Number.Natural.even n ⇔
Number.Natural.mod n
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)) =
Number.Numeral.zero
⊦ ∀n.
¬(n = Number.Numeral.zero) ⇒
Number.Natural.mod Number.Numeral.zero n = Number.Numeral.zero
⊦ ∀P. ¬(∀x. P x) ⇔ ∃x. ¬P x
⊦ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ ∀a a'. Data.Option.some a = Data.Option.some a' ⇔ a = a'
⊦ ∀m n. Number.Natural.< m n ⇒ Number.Natural.div m n = Number.Numeral.zero
⊦ ∀m n. Number.Natural.< m n ⇒ Number.Natural.mod m n = m
⊦ ∀m n.
Number.Natural.< m (Number.Natural.+ m n) ⇔
Number.Natural.< Number.Numeral.zero n
⊦ ∀m n. Number.Natural.suc m = Number.Natural.suc n ⇔ m = n
⊦ ∀m n.
Number.Natural.< (Number.Natural.suc m) (Number.Natural.suc n) ⇔
Number.Natural.< m n
⊦ ∀m n.
Number.Natural.≤ (Number.Natural.suc m) (Number.Natural.suc n) ⇔
Number.Natural.≤ m n
⊦ ∀m n. Number.Natural.+ m n = m ⇔ n = Number.Numeral.zero
⊦ ∀m n. Number.Natural.- m n = Number.Numeral.zero ⇔ Number.Natural.≤ m n
⊦ ∀n.
Number.Natural.odd n ⇔
Number.Natural.mod n
(Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)) =
Number.Numeral.bit1 Number.Numeral.zero
⊦ ∀m.
Number.Natural.- Number.Numeral.zero m = Number.Numeral.zero ∧
Number.Natural.- m Number.Numeral.zero = m
⊦ ∀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
⊦ ∀m n.
¬(n = Number.Numeral.zero) ⇒
Number.Natural.< (Number.Natural.mod m n) n
⊦ ∀m n.
¬(n = Number.Numeral.zero) ⇒
Number.Natural.≤ (Number.Natural.div m n) m
⊦ ∀m n.
¬(n = Number.Numeral.zero) ⇒
Number.Natural.≤ (Number.Natural.mod m n) m
⊦ ∀l m.
Data.List.length (Data.List.@ l m) =
Number.Natural.+ (Data.List.length l) (Data.List.length m)
⊦ ∀P. (∀p. P p) ⇔ ∀p1 p2. P (Data.Pair., p1 p2)
⊦ ∀m n. Number.Natural.≤ m n ⇔ ∃d. n = Number.Natural.+ m d
⊦ ∀l. l = Data.List.[] ∨ ∃h t. l = Data.List.:: h t
⊦ ∀f g. f = g ⇔ ∀x. f x = g x
⊦ ∀P a. (∃x. a = x ∧ P x) ⇔ P a
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ (Number.Natural.even Number.Numeral.zero ⇔ T) ∧
∀n. Number.Natural.even (Number.Natural.suc n) ⇔ ¬Number.Natural.even n
⊦ (Number.Natural.odd Number.Numeral.zero ⇔ F) ∧
∀n. Number.Natural.odd (Number.Natural.suc n) ⇔ ¬Number.Natural.odd n
⊦ ∀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
⊦ ∀n l.
Number.Natural.≤ n (Data.List.length l) ⇒
Data.List.length (Data.List.take n l) = n
⊦ ∀PAIR'. ∃fn. ∀a0 a1. fn (Data.Pair., a0 a1) = PAIR' a0 a1
⊦ ∀m n.
Number.Natural.< m n ⇔
∃d. n = Number.Natural.+ m (Number.Natural.suc d)
⊦ ∀P. (∀x y. P x y) ⇔ ∀y x. P x y
⊦ ∀P Q. (∃x. P ∧ Q x) ⇔ P ∧ ∃x. Q x
⊦ ∀P Q. P ∧ (∃x. Q x) ⇔ ∃x. P ∧ Q x
⊦ ∀P Q. P ∨ (∃x. Q x) ⇔ ∃x. P ∨ Q x
⊦ ∀m n.
¬(m = Number.Numeral.zero) ⇒
Number.Natural.div (Number.Natural.* m n) m = n
⊦ ∀m n.
¬(m = Number.Numeral.zero) ⇒
Number.Natural.mod (Number.Natural.* m n) m = Number.Numeral.zero
⊦ ∀P Q. (∀x. P x ∨ Q) ⇔ (∀x. P x) ∨ Q
⊦ ∀P Q. (∃x. P x) ∧ Q ⇔ ∃x. P x ∧ Q
⊦ ∀P Q. (∀x. P x) ∨ Q ⇔ ∀x. P x ∨ Q
⊦ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q
⊦ ∀x y z. x = y ∧ y = z ⇒ x = z
⊦ ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3
⊦ ∀t1 t2 t3. t1 ∨ t2 ∨ t3 ⇔ (t1 ∨ t2) ∨ t3
⊦ ∀p q r. p ∧ q ⇒ r ⇔ p ⇒ q ⇒ r
⊦ ∀n x i.
Number.Natural.< i n ⇒ Data.List.nth i (Data.List.replicate n x) = x
⊦ ∀m n p.
Number.Natural.* m (Number.Natural.* n p) =
Number.Natural.* (Number.Natural.* m n) p
⊦ ∀m n p.
Number.Natural.+ m (Number.Natural.+ n p) =
Number.Natural.+ (Number.Natural.+ m n) p
⊦ ∀m n p. Number.Natural.+ m n = Number.Natural.+ m p ⇔ n = p
⊦ ∀m n p. Number.Natural.+ m p = Number.Natural.+ n p ⇔ m = n
⊦ ∀m n p.
Number.Natural.< (Number.Natural.+ m n) (Number.Natural.+ m p) ⇔
Number.Natural.< n p
⊦ ∀m n p.
Number.Natural.≤ (Number.Natural.+ m n) (Number.Natural.+ m p) ⇔
Number.Natural.≤ n p
⊦ ∀m n p.
Number.Natural.≤ (Number.Natural.+ m p) (Number.Natural.+ n p) ⇔
Number.Natural.≤ m n
⊦ ∀m n p.
Number.Natural.- (Number.Natural.+ m n) (Number.Natural.+ m p) =
Number.Natural.- n p
⊦ ∀m n p.
Number.Natural.< m n ∧ Number.Natural.≤ n p ⇒ Number.Natural.< m p
⊦ ∀m n p.
Number.Natural.≤ m n ∧ Number.Natural.< n p ⇒ Number.Natural.< m p
⊦ ∀m n p.
Number.Natural.≤ m n ∧ Number.Natural.≤ n p ⇒ Number.Natural.≤ m p
⊦ ∀P x. (∀y. P y ⇔ y = x) ⇒ (select) P = x
⊦ ∀P. (∀x. ∃y. P x y) ⇔ ∃y. ∀x. P x (y x)
⊦ ∀t1 t2. (if T then t1 else t2) = t1 ∧ (if F then t1 else t2) = t2
⊦ ∀m n.
Number.Natural.* m n = Number.Numeral.zero ⇔
m = Number.Numeral.zero ∨ n = Number.Numeral.zero
⊦ ∀m n.
Number.Natural.+ m n = Number.Numeral.zero ⇔
m = Number.Numeral.zero ∧ n = Number.Numeral.zero
⊦ Data.List.length Data.List.[] = Number.Numeral.zero ∧
∀h t.
Data.List.length (Data.List.:: h t) =
Number.Natural.suc (Data.List.length t)
⊦ ∀P.
P Number.Numeral.zero ∧ (∀n. P n ⇒ P (Number.Natural.suc n)) ⇒ ∀n. P n
⊦ (∀t. ¬¬t ⇔ t) ∧ (¬T ⇔ F) ∧ (¬F ⇔ T)
⊦ ∀m n.
¬(n = Number.Numeral.zero) ⇒
(Number.Natural.div m n = Number.Numeral.zero ⇔ Number.Natural.< m n)
⊦ ∀m n.
¬(n = Number.Numeral.zero) ⇒
Number.Natural.mod (Number.Natural.mod m n) n = Number.Natural.mod m n
⊦ ∀m n.
Number.Natural.exp m n = Number.Numeral.zero ⇔
m = Number.Numeral.zero ∧ ¬(n = Number.Numeral.zero)
⊦ ∀b t1 t2. (if b then t1 else t2) ⇔ (¬b ∨ t1) ∧ (b ∨ t2)
⊦ ∀m n i.
Number.Natural.< i n ⇒
Data.List.nth i (Data.List.interval m n) = Number.Natural.+ m i
⊦ ∀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.* 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)
⊦ ∀m n p.
Number.Natural.* (Number.Natural.- m n) p =
Number.Natural.- (Number.Natural.* m p) (Number.Natural.* n p)
⊦ ∀b f x y. f (if b then x else y) = if b then f x else f y
⊦ ∀b f g x. (if b then f else g) x = if b then f x else g x
⊦ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x
⊦ ∀P Q. (∃x. P x ∨ Q x) ⇔ (∃x. P x) ∨ ∃x. Q x
⊦ ∀P Q. (∀x. P x ⇒ Q x) ⇒ (∀x. P x) ⇒ ∀x. Q x
⊦ ∀P Q. (∀x. P x ⇒ Q x) ⇒ (∃x. P x) ⇒ ∃x. Q x
⊦ ∀P Q. (∀x. P x) ∧ (∀x. Q x) ⇔ ∀x. P x ∧ Q x
⊦ ∀P Q. (∃x. P x) ∨ (∃x. Q x) ⇔ ∃x. P x ∨ Q x
⊦ ∀e f.
∃fn.
fn Number.Numeral.zero = e ∧
∀n. fn (Number.Natural.suc n) = f (fn n) n
⊦ ∀m n.
¬(n = Number.Numeral.zero) ⇒
Number.Natural.+ (Number.Natural.* (Number.Natural.div m n) n)
(Number.Natural.mod m n) = m
⊦ ∀P. P Data.List.[] ∧ (∀a0 a1. P a1 ⇒ P (Data.List.:: a0 a1)) ⇒ ∀x. P x
⊦ ∀<< <<<.
(∀x y. << x y ⇒ <<< x y) ∧ Relation.wellFounded <<< ⇒
Relation.wellFounded <<
⊦ ∀m n p.
Number.Natural.* m n = Number.Natural.* m p ⇔
m = Number.Numeral.zero ∨ n = p
⊦ ∀m n p.
Number.Natural.≤ (Number.Natural.* m n) (Number.Natural.* m p) ⇔
m = Number.Numeral.zero ∨ Number.Natural.≤ n p
⊦ ∀m n p.
Number.Natural.≤ (Number.Natural.* m p) (Number.Natural.* n p) ⇔
Number.Natural.≤ m n ∨ p = Number.Numeral.zero
⊦ ∀f l i.
Number.Natural.< i (Data.List.length l) ⇒
Data.List.nth i (Data.List.map f l) = f (Data.List.nth i l)
⊦ ∀m n p.
Number.Natural.< (Number.Natural.* m n) (Number.Natural.* m p) ⇔
¬(m = Number.Numeral.zero) ∧ Number.Natural.< n p
⊦ (∀x. Data.List.replicate Number.Numeral.zero x = Data.List.[]) ∧
∀n x.
Data.List.replicate (Number.Natural.suc n) x =
Data.List.:: x (Data.List.replicate n x)
⊦ ∀h1 h2 t1 t2. Data.List.:: h1 t1 = Data.List.:: h2 t2 ⇔ h1 = h2 ∧ t1 = t2
⊦ ∀x y a b. Data.Pair., x y = Data.Pair., a b ⇔ x = a ∧ y = b
⊦ ∀A B C D. (A ⇒ B) ∧ (C ⇒ D) ⇒ A ∧ C ⇒ B ∧ D
⊦ ∀A B C D. (A ⇒ B) ∧ (C ⇒ D) ⇒ A ∨ C ⇒ B ∨ D
⊦ ∀m n p q.
Number.Natural.< m p ∧ Number.Natural.< n q ⇒
Number.Natural.< (Number.Natural.+ m n) (Number.Natural.+ p q)
⊦ ∀m n p q.
Number.Natural.≤ m n ∧ Number.Natural.≤ p q ⇒
Number.Natural.≤ (Number.Natural.* m p) (Number.Natural.* n q)
⊦ ∀m n p q.
Number.Natural.≤ m p ∧ Number.Natural.≤ n q ⇒
Number.Natural.≤ (Number.Natural.+ m n) (Number.Natural.+ p q)
⊦ ∀P. (∀x. ∃!y. P x y) ⇔ ∃f. ∀x y. P x y ⇔ f x = y
⊦ (∀m. Data.List.interval m Number.Numeral.zero = Data.List.[]) ∧
∀m n.
Data.List.interval m (Number.Natural.suc n) =
Data.List.:: m (Data.List.interval (Number.Natural.suc m) n)
⊦ (∀m.
Number.Natural.exp m Number.Numeral.zero =
Number.Numeral.bit1 Number.Numeral.zero) ∧
∀m n.
Number.Natural.exp m (Number.Natural.suc n) =
Number.Natural.* m (Number.Natural.exp m n)
⊦ ∀P c x y. P (if c then x else y) ⇔ (c ⇒ P x) ∧ (¬c ⇒ P y)
⊦ (∀l. Data.List.drop Number.Numeral.zero l = l) ∧
∀n h t.
Data.List.drop (Number.Natural.suc n) (Data.List.:: h t) =
Data.List.drop n t
⊦ ∀NIL' CONS'.
∃fn.
fn Data.List.[] = NIL' ∧
∀a0 a1. fn (Data.List.:: a0 a1) = CONS' a0 a1 (fn a1)
⊦ ∀m n p.
¬(n = Number.Numeral.zero) ⇒
Number.Natural.mod (Number.Natural.* m (Number.Natural.mod p n)) n =
Number.Natural.mod (Number.Natural.* m p) n
⊦ ∀m n p.
¬(Number.Natural.* n p = Number.Numeral.zero) ⇒
Number.Natural.div (Number.Natural.div m n) p =
Number.Natural.div m (Number.Natural.* n p)
⊦ ∀m n p.
¬(Number.Natural.* n p = Number.Numeral.zero) ⇒
Number.Natural.mod (Number.Natural.mod m (Number.Natural.* n p)) n =
Number.Natural.mod m n
⊦ ∀n l i.
Number.Natural.≤ n (Data.List.length l) ∧ Number.Natural.< i n ⇒
Data.List.nth i (Data.List.take n l) = Data.List.nth i l
⊦ ∀P. (∃!x. P x) ⇔ (∃x. P x) ∧ ∀x x'. P x ∧ P x' ⇒ x = x'
⊦ ∀<<.
Relation.wellFounded << ⇔ ∀P. (∀x. (∀y. << y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x
⊦ (∀m. Number.Natural.< m Number.Numeral.zero ⇔ F) ∧
∀m n.
Number.Natural.< m (Number.Natural.suc n) ⇔
m = n ∨ Number.Natural.< m n
⊦ (∀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. Data.List.@ Data.List.[] l = l) ∧
∀h t l.
Data.List.@ (Data.List.:: h t) l = Data.List.:: h (Data.List.@ t l)
⊦ ∀t1 t2. (¬(t1 ∧ t2) ⇔ ¬t1 ∨ ¬t2) ∧ (¬(t1 ∨ t2) ⇔ ¬t1 ∧ ¬t2)
⊦ (∀l. Data.List.take Number.Numeral.zero l = Data.List.[]) ∧
∀n h t.
Data.List.take (Number.Natural.suc n) (Data.List.:: h t) =
Data.List.:: h (Data.List.take n t)
⊦ (∀f. Data.List.map f Data.List.[] = Data.List.[]) ∧
∀f h t.
Data.List.map f (Data.List.:: h t) =
Data.List.:: (f h) (Data.List.map f t)
⊦ ∀m n p.
¬(n = Number.Numeral.zero) ⇒
Number.Natural.mod
(Number.Natural.* (Number.Natural.mod m n) (Number.Natural.mod p n))
n = Number.Natural.mod (Number.Natural.* m p) n
⊦ ∀a b n.
¬(n = Number.Numeral.zero) ⇒
Number.Natural.mod
(Number.Natural.+ (Number.Natural.mod a n) (Number.Natural.mod b n))
n = Number.Natural.mod (Number.Natural.+ a b) n
⊦ ∀m n p.
¬(Number.Natural.* n p = Number.Numeral.zero) ⇒
Number.Natural.mod (Number.Natural.div m n) p =
Number.Natural.div (Number.Natural.mod m (Number.Natural.* n p)) n
⊦ ∀k l m.
Data.List.nth k (Data.List.@ l m) =
if Number.Natural.< k (Data.List.length l) then Data.List.nth k l
else Data.List.nth (Number.Natural.- k (Data.List.length l)) m
⊦ (∀m. Number.Natural.≤ m Number.Numeral.zero ⇔ m = Number.Numeral.zero) ∧
∀m n.
Number.Natural.≤ m (Number.Natural.suc n) ⇔
m = Number.Natural.suc n ∨ Number.Natural.≤ m n
⊦ (∀h t. Data.List.nth Number.Numeral.zero (Data.List.:: h t) = h) ∧
∀h t n.
Data.List.nth (Number.Natural.suc n) (Data.List.:: h t) =
Data.List.nth n t
⊦ ∀t. ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬t) ∧ ((t ⇔ F) ⇔ ¬t)
⊦ ∀l m.
Data.List.length l = Data.List.length m ∧
(∀i.
Number.Natural.< i (Data.List.length l) ⇒
Data.List.nth i l = Data.List.nth i m) ⇒ l = m
⊦ ∀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
⊦ ∀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)
⊦ ∀x m n.
Number.Natural.≤ (Number.Natural.exp x m) (Number.Natural.exp x n) ⇔
if x = Number.Numeral.zero then
m = Number.Numeral.zero ⇒ n = Number.Numeral.zero
else x = Number.Numeral.bit1 Number.Numeral.zero ∨ Number.Natural.≤ m n
⊦ (∀f. Data.List.zipWith f Data.List.[] Data.List.[] = Data.List.[]) ∧
∀f h1 h2 t1 t2.
Data.List.zipWith f (Data.List.:: h1 t1) (Data.List.:: h2 t2) =
Data.List.:: (f h1 h2) (Data.List.zipWith f t1 t2)
⊦ ∀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)
⊦ ∀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)
⊦ ∀a b n.
¬(n = Number.Numeral.zero) ⇒
(Number.Natural.mod (Number.Natural.+ a b) n =
Number.Natural.+ (Number.Natural.mod a n) (Number.Natural.mod b n) ⇔
Number.Natural.div (Number.Natural.+ a b) n =
Number.Natural.+ (Number.Natural.div a n) (Number.Natural.div b n))
⊦ ∀<<.
Relation.wellFounded << ⇒
∀H.
(∀f g x. (∀z. << z x ⇒ f z = g z) ⇒ H f x = H g x) ⇒
∃f. ∀x. f x = H f x
⊦ (∀n. Number.Natural.+ Number.Numeral.zero n = n) ∧
(∀m. Number.Natural.+ m Number.Numeral.zero = 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)
⊦ ∀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.* Number.Numeral.zero n = Number.Numeral.zero) ∧
(∀m. Number.Natural.* m Number.Numeral.zero = Number.Numeral.zero) ∧
(∀n. Number.Natural.* (Number.Numeral.bit1 Number.Numeral.zero) n = n) ∧
(∀m. Number.Natural.* m (Number.Numeral.bit1 Number.Numeral.zero) = 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)