Package base: The standard theory library

Information

Files

• Package tarball base-1.169.tgz
• Theory source file base.thy (included in the package tarball)

Defined Type Operators

• Data
  • List
    • list
  • Option
    • option
  • Pair
    • ×
  • Sum
    • +
  • Unit
    • unit
• Number
  • Natural
    • natural
  • Real
    • real
• Set
  • set

Defined Constants

• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∃!
    • ∨
    • ¬
    • cond
    • ⊥
    • ⊤
  • List
    • ::
    • @
    • []
    • all
    • any
    • case
    • concat
    • drop
    • filter
    • foldl
    • foldr
    • fromSet
    • head
    • interval
    • last
    • length
    • map
    • member
    • nth
    • nub
    • nubReverse
    • null
    • replicate
    • reverse
    • tail
    • take
    • toSet
    • zip
    • zipWith
  • Option
    • case
    • isNone
    • isSome
    • map
    • none
    • some
  • Pair
    • ,
    • fst
    • snd
  • Sum
    • case
    • destLeft
    • destRight
    • isLeft
    • isRight
    • left
    • right
  • Unit
    • ()
• Function
  • ↑
  • const
  • flip
  • id
  • injective
  • ∘
  • surjective
  • Combinator
    • Combinator.s
    • Combinator.w
• Number
  • Natural
    • *
    • +
    • -
    • <
    • ≤
    • >
    • ≥
    • ↑
    • bit0
    • bit1
    • distance
    • div
    • even
    • factorial
    • isSuc
    • log
    • max
    • min
    • minimal
    • mod
    • odd
    • pre
    • suc
    • zero
  • Real
    • *
    • +
    • -
    • /
    • <
    • ≤
    • >
    • ≥
    • ↑
    • ~
    • abs
    • fromNatural
    • inv
    • max
    • min
    • sup
• Relation
  • bigIntersect
  • bigUnion
  • empty
  • fromSet
  • intersect
  • irreflexive
  • measure
  • reflexive
  • subrelation
  • toSet
  • transitive
  • transitiveClosure
  • union
  • universe
  • wellFounded
• Set
  • ∅
  • bigIntersect
  • bigUnion
  • bijections
  • choice
  • cross
  • delete
  • \
  • disjoint
  • finite
  • fold
  • fromPredicate
  • hasSize
  • image
  • infinite
  • injections
  • insert
  • ∩
  • ∈
  • ⊂
  • rest
  • singleton
  • size
  • ⊆
  • surjections
  • ∪
  • universe

Theorems

⊦ ⊤

⊦ null []

⊦ isNone none

⊦ even 0

⊦ irreflexive empty

⊦ irreflexive isSuc

⊦ reflexive universe

⊦ transitive empty

⊦ transitive universe

⊦ transitive (<)

⊦ wellFounded empty

⊦ wellFounded (<)

⊦ wellFounded isSuc

⊦ finite ∅

⊦ finite universe

⊦ infinite universe

⊦ ¬isSome none

⊦ ¬odd 0

⊦ subrelation isSuc (<)

⊦ id = λx. x

⊦ ¬(universe = ∅)

⊦ const = λx y. x

⊦ empty = fromSet ∅

⊦ universe = fromSet universe

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ length [] = 0

⊦ bit0 0 = 0

⊦ size ∅ = 0

⊦ concat [] = []

⊦ nubReverse [] = []

⊦ reverse [] = []

⊦ toSet [] = ∅

⊦ bigIntersect ∅ = universe

⊦ bigUnion ∅ = ∅

⊦ transitiveClosure isSuc = (<)

⊦ map id = id

⊦ map id = id

⊦ ∀a. isSome (some a)

⊦ ∀a. isLeft (left a)

⊦ ∀x. x = x

⊦ ∀x. x ∈ universe

⊦ ∀b. isRight (right b)

⊦ ∀t. t ⇒ t

⊦ ∀v. v = ()

⊦ ∀n. 0 ≤ n

⊦ ∀n. n ≤ n

⊦ ∀x. x ≤ x

⊦ ∀l. finite (toSet l)

⊦ ∀s. disjoint ∅ s

⊦ ∀s. disjoint s ∅

⊦ ∀s. ∅ ⊆ s

⊦ ∀s. s ⊆ universe

⊦ ∀s. s ⊆ s

⊦ ∀p. all p []

⊦ ∀m. wellFounded (measure m)

⊦ ∀r. transitive (transitiveClosure r)

⊦ ∀r. subrelation r r

⊦ ⊥ ⇔ ∀p. p

⊦ (minimal n. ⊤) = 0

⊦ fromPredicate (λx. ⊥) = ∅

⊦ fromPredicate (λx. ⊤) = universe

⊦ ∀l. all (λx. ⊤) l

⊦ hasSize universe 2

⊦ factorial 0 = 1

⊦ cross universe universe = universe

⊦ ∀a. ¬isNone (some a)

⊦ ∀a. ¬isRight (left a)

⊦ ∀x. ¬member x []

⊦ ∀x. ¬(x ∈ ∅)

⊦ ∀a. finite (insert a ∅)

⊦ ∀x. id x = x

⊦ ∀b. ¬isLeft (right b)

⊦ ∀t. t ∨ ¬t

⊦ ∀m. ¬(m < 0)

⊦ ∀n. ¬(n < n)

⊦ ∀n. 0 < suc n

⊦ ∀n. n < suc n

⊦ ∀n. n ≤ suc n

⊦ ∀s. ¬(universe ⊂ s)

⊦ ∀s. ¬(s ⊂ ∅)

⊦ ∀s. ¬(s ⊂ s)

⊦ ∀p. ¬any p []

⊦ ∀r. subrelation r (transitiveClosure r)

⊦ (¬) = λp. p ⇒ ⊥

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

⊦ ∀x y. universe x y

⊦ ∀a. ∃x. x = a

⊦ ∀a. ∃!x. x = a

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

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

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

⊦ ∀f g. f = g

⊦ ⊤ ⇔ (λp. p) = λp. p

⊦ (∀) = λp. p = λx. ⊤

⊦ Combinator.w = λf x. f x x

⊦ ∀a. ¬(some a = none)

⊦ ∀a. destLeft (left a) = a

⊦ ∀x. replicate x 0 = []

⊦ ∀x. delete ∅ x = ∅

⊦ ∀x. insert x universe = universe

⊦ ∀b. destRight (right b) = b

⊦ ∀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. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. t ∨ ⊥ ⇔ t

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

⊦ ∀t. t ∨ t ⇔ t

⊦ ∀n. ¬(factorial n = 0)

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. n ≤ n * n

⊦ ∀n. even n ∨ odd n

⊦ ∀n. pre (suc n) = n

⊦ ∀n. 0 * n = 0

⊦ ∀m. m * 0 = 0

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀m. m - 0 = m

⊦ ∀n. n - n = 0

⊦ ∀n. distance 0 n = n

⊦ ∀n. distance n 0 = n

⊦ ∀n. distance n n = 0

⊦ ∀n. max 0 n = n

⊦ ∀n. max n 0 = n

⊦ ∀n. max n n = n

⊦ ∀n. min 0 n = 0

⊦ ∀n. min n 0 = 0

⊦ ∀n. min n n = n

⊦ ∀m. interval m 0 = []

⊦ ∀n. id ↑ n = id

⊦ ∀l. reverse (reverse l) = l

⊦ ∀l. [] @ l = l

⊦ ∀l. l @ [] = l

⊦ ∀l. drop 0 l = l

⊦ ∀l. take 0 l = []

⊦ ∀s. ∅ \ s = ∅

⊦ ∀s. s \ ∅ = s

⊦ ∀s. s \ universe = ∅

⊦ ∀s. s \ s = ∅

⊦ ∀s. image id s = s

⊦ ∀s. ∅ ∩ s = ∅

⊦ ∀s. universe ∩ s = s

⊦ ∀s. s ∩ ∅ = ∅

⊦ ∀s. s ∩ universe = s

⊦ ∀s. s ∩ s = s

⊦ ∀s. ∅ ∪ s = s

⊦ ∀s. universe ∪ s = universe

⊦ ∀s. s ∪ ∅ = s

⊦ ∀s. s ∪ universe = universe

⊦ ∀s. s ∪ s = s

⊦ ∀f. f ↑ 0 = id

⊦ ∀f. map f [] = []

⊦ ∀f. map f none = none

⊦ ∀f. image f ∅ = ∅

⊦ ∀x. Combinator.s const x = id

⊦ ∀f. f ∘ id = f

⊦ ∀f. id ∘ f = f

⊦ ∀p. filter p [] = []

⊦ ∀s. toSet (fromSet s) = s

⊦ ∀r. wellFounded r ⇒ irreflexive r

⊦ ∀f. flip (flip f) = f

⊦ ∀r. fromSet (toSet r) = r

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

⊦ flip = λf x y. f y x

⊦ ∀x y. ¬empty x y

⊦ ∀e. ∃fn. fn () = e

⊦ ∀e. ∃!fn. fn () = e

⊦ ∀l. map (λx. x) l = l

⊦ ∀s. image (λx. x) s = s

⊦ universe = insert ⊤ (insert ⊥ ∅)

⊦ size = fold (λx n. suc n) 0

⊦ ∀t₁ t₂. (let x ← t₂ in t₁) = t₁

⊦ ∀x. hasSize (insert x ∅) 1

⊦ ∀x. last (x :: []) = x

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

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

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀n. ¬(even n ∧ odd n)

⊦ ∀n. even (2 * n)

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

⊦ ∀n. ¬even n ⇔ odd n

⊦ ∀n. ¬odd n ⇔ even n

⊦ ∀m. m ↑ 0 = 1

⊦ ∀m. m * 1 = m

⊦ ∀n. n ↑ 1 = n

⊦ ∀n. n div 1 = n

⊦ ∀n. n mod 1 = 0

⊦ ∀m. 1 * m = m

⊦ ∀x. 0 + x = x

⊦ ∀l. null l ⇔ l = []

⊦ ∀l. length (reverse l) = length l

⊦ ∀l. nub (nub l) = nub l

⊦ ∀l. nubReverse (nubReverse l) = nubReverse l

⊦ ∀l. toSet (nub l) = toSet l

⊦ ∀l. toSet (nubReverse l) = toSet l

⊦ ∀l. toSet (reverse l) = toSet l

⊦ ∀l. length (nub l) ≤ length l

⊦ ∀l. length (nubReverse l) ≤ length l

⊦ ∀l. size (toSet l) ≤ length l

⊦ ∀l. drop (length l) l = []

⊦ ∀l. take (length l) l = l

⊦ ∀l. case [] (::) l = l

⊦ ∀l. foldr (::) [] l = l

⊦ ∀x. case none some x = x

⊦ ∀s. infinite s ⇔ ¬finite s

⊦ ∀s. bigIntersect (insert s ∅) = s

⊦ ∀s. bigUnion (insert s ∅) = s

⊦ ∀f. f ↑ 1 = f

⊦ ∀x. case left right x = x

⊦ ∀f. zipWith f [] [] = []

⊦ ∃f. injective f ∧ ¬surjective f

⊦ Combinator.s = λf g x. f x (g x)

⊦ ∀x y. const x y = x

⊦ ∀h t. ¬null (h :: t)

⊦ ∀x s. x ∈ insert x s

⊦ ∀x s. delete s x ⊆ s

⊦ ∀x. (select y. y = x) = x

⊦ ∀m n. m ≤ m + n

⊦ ∀m n. m ≤ max m n

⊦ ∀m n. n ≤ m + n

⊦ ∀m n. n ≤ max m n

⊦ ∀m n. min m n ≤ m

⊦ ∀m n. min m n ≤ n

⊦ ∀l. all (λx. ⊥) l ⇔ null l

⊦ ∀s t. disjoint s (t \ s)

⊦ ∀s t. s ⊆ s ∪ t

⊦ ∀s t. s ⊆ t ∪ s

⊦ ∀s t. disjoint (t \ s) s

⊦ ∀s t. s \ t ⊆ s

⊦ ∀s t. s ∩ t ⊆ s

⊦ ∀s t. t ∩ s ⊆ s

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

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

⊦ finite universe ∧ finite universe ⇒ finite universe

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

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

⊦ ∀n. odd (suc (2 * n))

⊦ ∀n. n < 2 ↑ n

⊦ ∀m. suc m = m + 1

⊦ ∀n. even (suc n) ⇔ ¬even n

⊦ ∀n. odd (suc n) ⇔ ¬odd n

⊦ ∀m. m ≤ 0 ⇔ m = 0

⊦ ∀n. 1 ↑ n = 1

⊦ ∀n. suc n - 1 = n

⊦ ∀x. x ↑ 0 = 1

⊦ ∀x. ~x + x = 0

⊦ ∀x. 1 * x = x

⊦ ∀l. nub l = reverse (nubReverse (reverse l))

⊦ ∀l. length l = 0 ⇔ null l

⊦ ∀l. toSet l = ∅ ⇔ null l

⊦ ∀s. finite s ⇔ hasSize s (size s)

⊦ ∀s. rest s = delete s (choice s)

⊦ ∀s. infinite s ⇒ ¬(s = ∅)

⊦ ∀s. disjoint s s ⇔ s = ∅

⊦ ∀s. hasSize s 0 ⇔ s = ∅

⊦ ∀s. universe ⊆ s ⇔ s = universe

⊦ ∀s. s ⊆ ∅ ⇔ s = ∅

⊦ ∀l. null (concat l) ⇔ all null l

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

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

⊦ ∀x n. length (replicate x n) = n

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

⊦ ∀h t. head (h :: t) = h

⊦ ∀h t. tail (h :: t) = t

⊦ ∀x s. ¬(insert x s = ∅)

⊦ ∀b f. case b f none = b

⊦ ∀b f. case b f [] = b

⊦ ∀b t. (if b then t else t) = t

⊦ ∀m n. ¬(m + n < m)

⊦ ∀m n. ¬(n + m < m)

⊦ ∀m n. length (interval m n) = n

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

⊦ ∀r x. reflexive r ⇒ r x x

⊦ ∀r. reflexive r ⇔ ∀x. r x x

⊦ ∀f b. foldr f b [] = b

⊦ ∀f b. foldl f b [] = b

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

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

⊦ ∀l. length l = 0 ⇔ l = []

⊦ ∀l. toSet l = ∅ ⇔ l = []

⊦ ∀l. foldl (flip (::)) [] l = reverse l

⊦ ∀s. finite s ⇒ toSet (fromSet s) = s

⊦ ∀f y. (let x ← y in f x) = f y

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

⊦ ∀s. bigIntersect s = fromSet (bigIntersect (image toSet s))

⊦ ∀s. bigUnion s = fromSet (bigUnion (image toSet s))

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

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

⊦ ∀h t. nth (h :: t) 0 = h

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

⊦ ∀t₁ t₂. t₁ ∧ t₂ ⇔ t₂ ∧ t₁

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

⊦ ∀a b. (a ⇔ b) ⇒ a ⇒ b

⊦ ∀m n. m > n ⇔ n < m

⊦ ∀m n. m ≥ n ⇔ n ≤ m

⊦ ∀m n. m * n = n * m

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

⊦ ∀m n. distance m n = distance n m

⊦ ∀m n. max m n = max n m

⊦ ∀m n. min m n = min n m

⊦ ∀m n. m = n ⇒ m ≤ n

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

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

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

⊦ ∀m n. m ≤ n ∨ n ≤ m

⊦ ∀m n. distance m n ≤ m + n

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

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

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

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

⊦ ∀m n. n * (m div n) ≤ m

⊦ ∀x y. x > y ⇔ y < x

⊦ ∀x y. x ≥ y ⇔ y ≤ x

⊦ ∀x y. x * y = y * x

⊦ ∀x y. x + y = y + x

⊦ ∀x y. x ≤ y ∨ y ≤ x

⊦ ∀s x. finite s ⇒ finite (delete s x)

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

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

⊦ ∀s t. finite s ⇒ finite (s \ t)

⊦ ∀s t. disjoint s t ⇔ disjoint t s

⊦ ∀s t. s ∩ t = t ∩ s

⊦ ∀s t. s ∪ t = t ∪ s

⊦ ∀s t. s ⊂ t ⇒ s ⊆ t

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

⊦ ∀s. finite s ⇒ ∃a. ¬(a ∈ s)

⊦ ∀f l. null (map f l) ⇔ null l

⊦ ∀f l. length (map f l) = length l

⊦ ∀f s. finite s ⇒ finite (image f s)

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

⊦ ∀p l. length (filter p l) ≤ length l

⊦ ∀f x. Combinator.w f x = f x x

⊦ ∀r x. irreflexive r ⇒ ¬r x x

⊦ ∀r. irreflexive r ⇔ ∀x. ¬r x x

⊦ ∅ = { x. x | ⊥ }

⊦ universe = { x. x | ⊤ }

⊦ ∀n. factorial (suc n) = suc n * factorial n

⊦ ∀n. n ↑ 2 = n * n

⊦ ∀n. 2 * n = n + n

⊦ ∀s. finite s ⇒ length (fromSet s) = size s

⊦ ∀s. ¬(s = ∅) ⇒ choice s ∈ s

⊦ ∀x n. null (replicate x n) ⇔ n = 0

⊦ ∀h t. length (h :: t) = suc (length t)

⊦ ∀m n. ¬(m < n ∧ n < m)

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

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

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

⊦ ∀m n. m < n ⇒ ¬(m = n)

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

⊦ ∀x y. x < y ⇔ ¬(y ≤ x)

⊦ ∀x y. x - y = x + ~y

⊦ ∀l x. member x l ⇔ x ∈ toSet l

⊦ ∀l x. member x (nub l) ⇔ member x l

⊦ ∀l x. member x (nubReverse l) ⇔ member x l

⊦ ∀l x. member x (reverse l) ⇔ member x l

⊦ ∀l₁ l₂. foldr (::) l₂ l₁ = l₁ @ l₂

⊦ ∀l₁ l₂. drop (length l₁) (l₁ @ l₂) = l₂

⊦ ∀l₁ l₂. take (length l₁) (l₁ @ l₂) = l₁

⊦ ∀l₁ l₂. zip l₁ l₂ = zipWith , l₁ l₂

⊦ ∀x. x = none ∨ ∃a. x = some a

⊦ ∀s n. hasSize s n ⇒ size s = n

⊦ ∀s. singleton s ⇔ ∃x. s = insert x ∅

⊦ ∀s. s ⊂ universe ⇔ ∃x. ¬(x ∈ s)

⊦ ∀s. (∃x. x ∈ s) ⇔ ¬(s = ∅)

⊦ ∀f a. map f (some a) = some (f a)

⊦ ∀p. (∀b. p b) ⇔ p ⊤ ∧ p ⊥

⊦ ∀p. (∃b. p b) ⇔ p ⊤ ∨ p ⊥

⊦ ∀p. p ⊥ ∧ p ⊤ ⇒ ∀x. p x

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

⊦ ∀n. even n ⇔ n mod 2 = 0

⊦ ∀n. ¬(n = 0) ⇒ 0 div n = 0

⊦ ∀n. ¬(n = 0) ⇒ 0 mod n = 0

⊦ ∀n. ¬(n = 0) ⇒ n mod n = 0

⊦ ∀f. surjective f ⇔ ∀y. ∃x. y = f x

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

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

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

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

⊦ ∀r. subrelation isSuc r ∧ transitive r ⇒ subrelation (<) r

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

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

⊦ ∀a a'. some a = some a' ⇔ a = a'

⊦ ∀h t. toSet (h :: t) = insert h (toSet t)

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

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

⊦ ∀x s. s \ insert x ∅ = delete s x

⊦ ∀x s. insert x (insert x s) = insert x s

⊦ ∀x s. delete (delete s x) x = delete s x

⊦ ∀x s. insert x ∅ ∪ s = insert x s

⊦ ∀p q. (q ⇒ p) ⇒ ¬p ⇒ ¬q

⊦ ∀t₁ t₂. ¬(t₁ ⇒ t₂) ⇔ t₁ ∧ ¬t₂

⊦ ∀t₁ t₂. (¬t₁ ⇔ ¬t₂) ⇔ t₁ ⇔ t₂

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

⊦ ∀m n. m < n ⇒ m div n = 0

⊦ ∀m n. m < n ⇒ m mod n = m

⊦ ∀m n. m ≤ n ⇒ factorial m ≤ factorial n

⊦ ∀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. fromNatural m = fromNatural n ⇔ m = n

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

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

⊦ ∀m n. fromNatural m ≤ fromNatural n ⇔ m ≤ n

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

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

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

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

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

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

⊦ ∀h t. concat (h :: t) = h @ concat t

⊦ ∀s x. insert x ∅ ⊆ s ⇔ x ∈ s

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

⊦ ∀s t. s ⊆ t ⇔ s ∩ t = s

⊦ ∀s t. s ⊆ t ⇔ s ∪ t = t

⊦ ∀s t. s \ t = ∅ ⇔ s ⊆ t

⊦ ∀s t. s \ t = s ⇔ disjoint s t

⊦ ∀s t. t ∪ (s \ t) = t ∪ s

⊦ ∀s t. s \ t \ t = s \ t

⊦ ∀s t. s \ t ∪ t = s ∪ t

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

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

⊦ ∀s u. bigIntersect (insert s u) = s ∩ bigIntersect u

⊦ ∀s u. bigUnion (insert s u) = s ∪ bigUnion u

⊦ ∀f l. reverse (map f l) = map f (reverse l)

⊦ ∀f l. toSet (map f l) = image f (toSet l)

⊦ ∀f l. map f l = [] ⇔ l = []

⊦ ∀f s. image f s = ∅ ⇔ s = ∅

⊦ ∀s t. s ⊆ t ⇒ bigIntersect t ⊆ bigIntersect s

⊦ ∀f g. f ⊆ g ⇒ bigUnion f ⊆ bigUnion g

⊦ ∀r s. subrelation r s ∧ wellFounded s ⇒ wellFounded r

⊦ ∀r s. subrelation r s ⇔ toSet r ⊆ toSet s

⊦ ∀r s. toSet r = toSet s ⇒ r = s

⊦ { m. m | m < 0 } = ∅

⊦ ∀b f a. case b f (some a) = f a

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

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

⊦ ∀n. odd n ⇔ n mod 2 = 1

⊦ ∀n. 0 ↑ n = if n = 0 then 1 else 0

⊦ ∀n. ¬(n = 0) ⇒ n div n = 1

⊦ ∀k. 1 < k ⇒ log k 1 = 0

⊦ ∀x. abs x = if 0 ≤ x then x else ~x

⊦ ∀l. ¬null l ⇒ head l :: tail l = l

⊦ ∀s. finite s ⇒ (size s = 0 ⇔ s = ∅)

⊦ ∀f g a. case f g (left a) = f a

⊦ ∀f g b. case f g (right b) = g b

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

⊦ ∀f x y. flip f x y = f y x

⊦ ∀x n. replicate x (suc n) = x :: replicate x n

⊦ ∀h t. take 1 (h :: t) = h :: []

⊦ ∀x s. disjoint s (insert x ∅) ⇔ ¬(x ∈ s)

⊦ ∀x s. delete s x = s ⇔ ¬(x ∈ s)

⊦ ∀x s. disjoint (insert x ∅) s ⇔ ¬(x ∈ s)

⊦ ∀t₁ t₂. ¬(t₁ ∧ t₂) ⇔ ¬t₁ ∨ ¬t₂

⊦ ∀t₁ t₂. ¬(t₁ ∨ t₂) ⇔ ¬t₁ ∧ ¬t₂

⊦ ∀m n. max m n = if m ≤ n then n else m

⊦ ∀m n. min m n = if m ≤ n then m else n

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

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

⊦ ∀m n. odd (m * n) ⇔ odd m ∧ odd n

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

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

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

⊦ ∀m n. ¬(n = 0) ⇒ m mod n < n

⊦ ∀m n. ¬(n = 0) ⇒ m div n ≤ m

⊦ ∀m n. ¬(n = 0) ⇒ m mod n ≤ m

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

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

⊦ ∀m n. fromNatural m * fromNatural n = fromNatural (m * n)