Package lazy-list: Lazy lists/colists/streams

Information

Files

• Package tarball lazy-list-0.1.tgz
• Theory file lazy-list.thy (included in the package tarball)

Defined Type Operator

• llist
  • llist.llist

Defined Constants

• llist
  • llist.every
  • llist.exists
  • llist.fromList
  • llist.linear_order_to_list_f
  • llist.llength_rel
  • llist.llist_abs
  • llist.llist_rep
  • llist.lrep_ok
  • llist.toList
  • llist.LAPPEND
  • llist.LCONS
  • llist.LDROP
  • llist.LFILTER
  • llist.LFINITE
  • llist.LFLATTEN
  • llist.LHD
  • llist.LLENGTH
  • llist.LMAP
  • llist.LNIL
  • llist.LNTH
  • llist.LTAKE
  • llist.LTL
  • llist.LUNFOLD
  • llist.LUNZIP
  • llist.LZIP
• Unwanted
  • Unwanted.id

Axiom

⊦ Data.Bool.let f v ⇔
  Data.Bool.∀
    (Function.Combinator.s
       (Function.∘ Data.Bool.⇒
          (Function.∘ Unwanted.id (Function.Combinator.c (=) v))) f)

Theorems

⊦ Data.Bool.∀ (λl. llist.LFINITE (llist.fromList l))

⊦ Data.Bool.∃ (λrep. HOL4.TYPE_DEFINITION llist.lrep_ok rep)

⊦ llist.LNIL = llist.llist_abs (λn. Data.Option.NONE)

⊦ llist.LDROP (Number.Numeral.bit1 Number.Numeral.zero) = llist.LTL

⊦ Data.Bool.∀ (λll. llist.LAPPEND ll llist.LNIL = ll)

⊦ Data.Bool.∀ (λll. llist.LZIP (llist.LUNZIP ll) = ll)

⊦ llist.LHD (llist.LCONS h t) = Data.Option.SOME h

⊦ llist.LTL (llist.LCONS h t) = Data.Option.SOME t

⊦ Data.Bool.∀ (λll. llist.LHD ll = llist.llist_rep ll Number.Numeral.zero)

⊦ Data.Bool.∀ (λh. llist.LFLATTEN (llist.LCONS h llist.LNIL) = h)

⊦ Data.Bool.∀ (λl. llist.toList (llist.fromList l) = Data.Option.SOME l)

⊦ Data.Bool.∀
    (λl.
       llist.LLENGTH (llist.fromList l) =
       Data.Option.SOME (Data.List.length l))

⊦ Data.Bool.∀
    (λll.
       Data.Bool.⇒ (Data.Bool.¬ (llist.LFINITE ll))
         (llist.LLENGTH ll = Data.Option.NONE))

⊦ Data.Bool.∀
    (λl.
       llist.LTAKE (Data.List.length l) (llist.fromList l) =
       Data.Option.SOME l)

⊦ llist.LFINITE ll ⇔ Data.Bool.∃ (λn. llist.LTAKE n ll = Data.Option.NONE)

⊦ Data.Bool.∀
    (λll.
       Data.Bool.∀
         (λf. llist.LLENGTH (llist.LMAP f ll) = llist.LLENGTH ll))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∀
         (λll. llist.LFINITE (llist.LMAP f ll) ⇔ llist.LFINITE ll))

⊦ Data.Bool.∀
    (λm.
       llist.LTAKE m llist.LNIL = Data.Option.NONE ⇔
       Number.Natural.< Number.Numeral.zero m)

⊦ Data.Bool.∀
    (λll.
       Data.Bool.⇒ (llist.LFINITE ll)
         (llist.fromList (Data.Option.the (llist.toList ll)) = ll))

⊦ Data.Bool.∀
    (λll. llist.LFLATTEN ll = llist.LNIL ⇔ llist.every ((=) llist.LNIL) ll)

⊦ Data.Bool.∀
    (λll.
       Data.Bool.⇒ (llist.LFINITE ll)
         (Data.Bool.∃ (λn. llist.LLENGTH ll = Data.Option.SOME n)))

⊦ Data.Bool.∀
    (λll.
       Data.Bool.⇒ (llist.LFINITE ll)
         (Data.Bool.∃ (λl. llist.toList ll = Data.Option.SOME l)))

⊦ Data.Bool.∀
    (λll1.
       Data.Bool.∀
         (λll2.
            Data.Bool.⇒ (Data.Bool.¬ (llist.LFINITE ll1))
              (llist.LAPPEND ll1 ll2 = ll1)))

⊦ Data.Bool.∀
    (λh.
       Data.Bool.∀
         (λt.
            llist.LFLATTEN (llist.LCONS h t) =
            llist.LAPPEND h (llist.LFLATTEN t)))

⊦ Data.Bool.∀
    (λll.
       llist.LFILTER P ll = llist.LNIL ⇔
       llist.every (Function.∘ Data.Bool.¬ P) ll)

⊦ Data.Bool.∀
    (λll1.
       Data.Bool.∀
         (λll2.
            llist.LFINITE (llist.LAPPEND ll1 ll2) ⇔
            Data.Bool.∧ (llist.LFINITE ll1) (llist.LFINITE ll2)))

⊦ Data.Bool.∀
    (λl1.
       Data.Bool.∀
         (λl2.
            llist.LAPPEND (llist.fromList l1) (llist.fromList l2) =
            llist.fromList (Data.List.@ l1 l2)))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λll.
            llist.every P ll ⇔
            Data.Bool.¬ (llist.exists (Function.∘ Data.Bool.¬ P) ll)))

⊦ Data.Bool.∧ (llist.LFINITE llist.LNIL)
    (Data.Bool.∀
       (λh.
          Data.Bool.∀
            (λt.
               Data.Bool.⇒ (llist.LFINITE t)
                 (llist.LFINITE (llist.LCONS h t)))))

⊦ llist.LAPPEND l1 l2 = llist.LNIL ⇔
  Data.Bool.∧ (l1 = llist.LNIL) (l2 = llist.LNIL)

⊦ Data.Bool.∀
    (λll.
       llist.toList ll =
       if llist.LFINITE ll then
         llist.LTAKE (Data.Option.the (llist.LLENGTH ll)) ll
       else Data.Option.NONE)

⊦ Data.Bool.∀
    (λl.
       Data.Bool.∨ (l = llist.LNIL)
         (Data.Bool.∃ (λh. Data.Bool.∃ (λt. l = llist.LCONS h t))))

⊦ Data.Bool.∀
    (λn.
       Data.Bool.∀
         (λll.
            Data.Bool.⇒ (llist.LTAKE n ll = Data.Option.NONE)
              (llist.LNTH n ll = Data.Option.NONE)))

⊦ Data.Bool.∀
    (λll.
       llist.LLENGTH ll =
       if llist.LFINITE ll then
         Data.Option.SOME (Data.Bool.select (λn. llist.llength_rel ll n))
       else Data.Option.NONE)

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λll.
            Data.Bool.⇒ (llist.every (Function.∘ Data.Bool.¬ P) ll)
              (llist.LFILTER P ll = llist.LNIL)))

⊦ Data.Bool.∀
    (λll.
       Data.Bool.⇒ (Data.Bool.¬ (llist.LFINITE ll))
         (Data.Bool.∀
            (λn. Data.Bool.∃ (λy. llist.LDROP n ll = Data.Option.SOME y))))

⊦ Data.Bool.∀
    (λll.
       Data.Bool.⇒ (Data.Bool.¬ (llist.LFINITE ll))
         (Data.Bool.∀
            (λn. Data.Bool.∃ (λy. llist.LTAKE n ll = Data.Option.SOME y))))

⊦ Data.Bool.⇒ (Data.Bool.∀ (λx. Data.Bool.⇒ (P x) (Q x)))
    (Data.Bool.⇒ (llist.every P l) (llist.every Q l))

⊦ Data.Bool.⇒ (Data.Bool.∀ (λx. Data.Bool.⇒ (P x) (Q x)))
    (Data.Bool.⇒ (llist.exists P l) (llist.exists Q l))

⊦ Data.Bool.∧ (llist.LFINITE llist.LNIL ⇔ Data.Bool.T)
    (Data.Bool.∀
       (λh.
          Data.Bool.∀
            (λt. llist.LFINITE (llist.LCONS h t) ⇔ llist.LFINITE t)))

⊦ Data.Bool.∧ (llist.LHD llist.LNIL = Data.Option.NONE)
    (Data.Bool.∀
       (λh.
          Data.Bool.∀
            (λt. llist.LHD (llist.LCONS h t) = Data.Option.SOME h)))

⊦ Data.Bool.∧ (llist.LTL llist.LNIL = Data.Option.NONE)
    (Data.Bool.∀
       (λh.
          Data.Bool.∀
            (λt. llist.LTL (llist.LCONS h t) = Data.Option.SOME t)))

⊦ Data.Bool.∀
    (λn.
       Data.Bool.∀
         (λll.
            Data.Bool.∀
              (λl.
                 Data.Bool.⇒ (llist.LTAKE n ll = Data.Option.SOME l)
                   (n = Data.List.length l))))

⊦ Data.Bool.∀
    (λll1.
       Data.Bool.∀
         (λll2.
            Data.Bool.∀
              (λll3.
                 llist.LAPPEND (llist.LAPPEND ll1 ll2) ll3 =
                 llist.LAPPEND ll1 (llist.LAPPEND ll2 ll3))))

⊦ Data.Bool.∀
    (λll1.
       Data.Bool.∀
         (λll2.
            ll1 = ll2 ⇔
            Data.Bool.∀ (λn. llist.LNTH n ll1 = llist.LNTH n ll2)))

⊦ Data.Bool.∀
    (λll1.
       Data.Bool.∀
         (λll2.
            ll1 = ll2 ⇔
            Data.Bool.∀ (λn. llist.LTAKE n ll1 = llist.LTAKE n ll2)))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∀
         (λg.
            Data.Bool.∀
              (λll.
                 llist.LMAP f (llist.LMAP g ll) =
                 llist.LMAP (Function.∘ f g) ll)))

⊦ Data.Bool.∀
    (λh.
       Data.Bool.∀
         (λt.
            Data.Bool.∧ (Data.Bool.¬ (llist.LCONS h t = llist.LNIL))
              (Data.Bool.¬ (llist.LNIL = llist.LCONS h t))))

⊦ Data.Bool.∀
    (λl.
       Data.Bool.∀
         (λm.
            llist.LTAKE m llist.LNIL = Data.Option.SOME l ⇔
            Data.Bool.∧ (m = Number.Numeral.zero) (l = Data.List.[])))

⊦ Data.Bool.∧ (llist.fromList Data.List.[] = llist.LNIL)
    (Data.Bool.∀
       (λh.
          Data.Bool.∀
            (λt.
               llist.fromList (Data.List.:: h t) =
               llist.LCONS h (llist.fromList t))))

⊦ Data.Bool.∧ (Data.Bool.∀ (λa. llist.llist_abs (llist.llist_rep a) = a))
    (Data.Bool.∀
       (λr. llist.lrep_ok r ⇔ llist.llist_rep (llist.llist_abs r) = r))

⊦ Data.Bool.∀
    (λll.
       llist.LTL ll =
       Data.Option.case Data.Option.NONE
         (λv.
            Data.Option.SOME
              (llist.llist_abs
                 (λn.
                    llist.llist_rep ll
                      (Number.Natural.+ n
                         (Number.Numeral.bit1 Number.Numeral.zero)))))
         (llist.LHD ll))

⊦ Data.Bool.∀
    (λl.
       llist.exists P l ⇔
       Data.Bool.∃
         (λn.
            Data.Bool.∃
              (λe.
                 Data.Bool.∧ (Data.Option.SOME e = llist.LNTH n l) (P e))))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∀
         (λll1.
            Data.Bool.∀
              (λll2.
                 llist.LMAP f (llist.LAPPEND ll1 ll2) =
                 llist.LAPPEND (llist.LMAP f ll1) (llist.LMAP f ll2))))

⊦ llist.llist_rep (llist.LCONS h t) =
  λn.
    if n = Number.Numeral.zero then Data.Option.SOME h
    else
      llist.llist_rep t
        (Number.Natural.- n (Number.Numeral.bit1 Number.Numeral.zero))

⊦ Data.Bool.∀
    (λh.
       Data.Bool.∀
         (λt.
            Data.Bool.∧ (llist.LHD (llist.LCONS h t) = Data.Option.SOME h)
              (llist.LTL (llist.LCONS h t) = Data.Option.SOME t)))

⊦ Data.Bool.∧
    (llist.LLENGTH llist.LNIL = Data.Option.SOME Number.Numeral.zero)
    (Data.Bool.∀
       (λh.
          Data.Bool.∀
            (λt.
               llist.LLENGTH (llist.LCONS h t) =
               Data.Option.map Number.Natural.suc (llist.LLENGTH t))))

⊦ Data.Bool.∧ (llist.every P llist.LNIL ⇔ Data.Bool.T)
    (llist.every P (llist.LCONS h t) ⇔ Data.Bool.∧ (P h) (llist.every P t))

⊦ Data.Bool.∧ (llist.exists P llist.LNIL ⇔ Data.Bool.F)
    (llist.exists P (llist.LCONS h t) ⇔
     Data.Bool.∨ (P h) (llist.exists P t))

⊦ Data.Bool.∀
    (λll.
       Data.Bool.∧ (llist.LHD ll = Data.Option.NONE ⇔ ll = llist.LNIL)
         (Data.Option.NONE = llist.LHD ll ⇔ ll = llist.LNIL))

⊦ Data.Bool.∀
    (λll.
       Data.Bool.∧ (llist.LTL ll = Data.Option.NONE ⇔ ll = llist.LNIL)
         (Data.Option.NONE = llist.LTL ll ⇔ ll = llist.LNIL))

⊦ Data.Bool.∧ (llist.llength_rel llist.LNIL Number.Numeral.zero)
    (Data.Bool.∀
       (λh.
          Data.Bool.∀
            (λn.
               Data.Bool.∀
                 (λt.
                    Data.Bool.⇒ (llist.llength_rel t n)
                      (llist.llength_rel (llist.LCONS h t)
                         (Number.Natural.suc n))))))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∃
         (λg.
            Data.Bool.∀
              (λx.
                 g x =
                 Data.Option.case llist.LNIL
                   (λv. Data.Pair.case (λa b. llist.LCONS b (g a)) v)
                   (f x))))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∃!
         (λg.
            Data.Bool.∀
              (λx.
                 g x =
                 Data.Option.case llist.LNIL
                   (λv. Data.Pair.case (λa b. llist.LCONS b (g a)) v)
                   (f x))))

⊦ Data.Bool.∧ (llist.toList llist.LNIL = Data.Option.SOME Data.List.[])
    (Data.Bool.∀
       (λh.
          Data.Bool.∀
            (λt.
               llist.toList (llist.LCONS h t) =
               Data.Option.map (Data.List.:: h) (llist.toList t))))

⊦ Data.Bool.∀
    (λn.
       Data.Bool.∀
         (λl.
            Data.Bool.∀
              (λx.
                 Data.Bool.⇒ (llist.LNTH n l = Data.Option.SOME x)
                   (llist.LHD (Data.Option.the (llist.LDROP n l)) =
                    Data.Option.SOME x))))

⊦ Data.Bool.∀
    (λn.
       Data.Bool.∀
         (λll.
            Data.Bool.⇒
              (Data.Bool.∧ (llist.LFINITE ll)
                 (Number.Natural.≤ n (Data.Option.the (llist.LLENGTH ll))))
              (Data.Bool.∃ (λy. llist.LDROP n ll = Data.Option.SOME y))))

⊦ Data.Bool.∀
    (λn.
       Data.Bool.∀
         (λll.
            Data.Bool.⇒
              (Data.Bool.∧ (llist.LFINITE ll)
                 (Number.Natural.≤ n (Data.Option.the (llist.LLENGTH ll))))
              (Data.Bool.∃ (λy. llist.LTAKE n ll = Data.Option.SOME y))))

⊦ Data.Bool.∀
    (λa0.
       llist.LFINITE a0 ⇔
       Data.Bool.∨ (a0 = llist.LNIL)
         (Data.Bool.∃
            (λh.
               Data.Bool.∃
                 (λt.
                    Data.Bool.∧ (a0 = llist.LCONS h t)
                      (llist.LFINITE t)))))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∀
         (λx.
            llist.LUNFOLD f x =
            Data.Option.case llist.LNIL
              (λv.
                 Data.Pair.case
                   (λv1 v2. llist.LCONS v2 (llist.LUNFOLD f v1)) v) (f x)))

⊦ llist.exists P ll ⇔
  Data.Bool.∃
    (λn.
       Data.Bool.∃
         (λa.
            Data.Bool.∃
              (λt.
                 Data.Bool.∧
                   (llist.LDROP n ll = Data.Option.SOME (llist.LCONS a t))
                   (P a))))

⊦ Data.Bool.∀
    (λh.
       Data.Bool.∀
         (λt.
            llist.LCONS h t =
            llist.llist_abs
              (λn.
                 if n = Number.Numeral.zero then Data.Option.SOME h
                 else
                   llist.llist_rep t
                     (Number.Natural.- n
                        (Number.Numeral.bit1 Number.Numeral.zero)))))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λll1.
            Data.Bool.∀
              (λll2.
                 Data.Bool.⇒ (llist.LFINITE ll1)
                   (llist.LFILTER P (llist.LAPPEND ll1 ll2) =
                    llist.LAPPEND (llist.LFILTER P ll1)
                      (llist.LFILTER P ll2)))))

⊦ Data.Bool.∀
    (λh1.
       Data.Bool.∀
         (λt1.
            Data.Bool.∀
              (λh2.
                 Data.Bool.∀
                   (λt2.
                      llist.LCONS h1 t1 = llist.LCONS h2 t2 ⇔
                      Data.Bool.∧ (h1 = h2) (t1 = t2)))))

⊦ Data.Bool.∀
    (λh.
       Data.Bool.∀
         (λt.
            Data.Bool.∀
              (λll.
                 ll = llist.LCONS h t ⇔
                 Data.Bool.∧ (llist.LHD ll = Data.Option.SOME h)
                   (llist.LTL ll = Data.Option.SOME t))))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∀
         (λg.
            Data.Bool.∀
              (λs.
                 llist.LMAP f (llist.LUNFOLD g s) =
                 llist.LUNFOLD
                   (λs.
                      Data.Option.map
                        (Data.Pair.uncurry (λx y. Data.Pair., x (f y)))
                        (g s)) s)))

⊦ Data.Bool.∀
    (λLFINITE'.
       Data.Bool.⇒
         (Data.Bool.∧ (LFINITE' llist.LNIL)
            (Data.Bool.∀
               (λh.
                  Data.Bool.∀
                    (λt.
                       Data.Bool.⇒ (LFINITE' t)
                         (LFINITE' (llist.LCONS h t))))))
         (Data.Bool.∀ (λa0. Data.Bool.⇒ (llist.LFINITE a0) (LFINITE' a0))))

⊦ Data.Bool.∀
    (λn.
       Data.Bool.∀
         (λl.
            Data.Bool.∀
              (λx.
                 Data.Bool.⇒ (llist.LTAKE n l = Data.Option.SOME x)
                   (Data.Bool.∀
                      (λh.
                         Data.Bool.∃
                           (λy.
                              llist.LTAKE n (llist.LCONS h l) =
                              Data.Option.SOME y))))))

⊦ Data.Bool.∧
    (Data.Bool.∀ (λll. llist.LNTH Number.Numeral.zero ll = llist.LHD ll))
    (Data.Bool.∀
       (λn.
          Data.Bool.∀
            (λll.
               llist.LNTH (Number.Natural.suc n) ll =
               Data.Option.join
                 (Data.Option.map (llist.LNTH n) (llist.LTL ll)))))

⊦ Data.Bool.∧
    (Data.Bool.∀
       (λll. llist.LDROP Number.Numeral.zero ll = Data.Option.SOME ll))
    (Data.Bool.∀
       (λn.
          Data.Bool.∀
            (λll.
               llist.LDROP (Number.Natural.suc n) ll =
               Data.Option.join
                 (Data.Option.map (llist.LDROP n) (llist.LTL ll)))))

⊦ Data.Bool.∀
    (λll1.
       Data.Bool.∀
         (λll2.
            llist.LLENGTH (llist.LAPPEND ll1 ll2) =
            if Data.Bool.∧ (llist.LFINITE ll1) (llist.LFINITE ll2) then
              Data.Option.SOME
                (Number.Natural.+ (Data.Option.the (llist.LLENGTH ll1))
                   (Data.Option.the (llist.LLENGTH ll2)))
            else Data.Option.NONE))

⊦ Data.Bool.∧ (Data.Bool.∀ (λx. llist.LAPPEND llist.LNIL x = x))
    (Data.Bool.∀
       (λh.
          Data.Bool.∀
            (λt.
               Data.Bool.∀
                 (λx.
                    llist.LAPPEND (llist.LCONS h t) x =
                    llist.LCONS h (llist.LAPPEND t x)))))

⊦ Data.Bool.⇒
    (Data.Bool.∧ (P llist.LNIL)
       (Data.Bool.∀
          (λh.
             Data.Bool.∀
               (λt.
                  Data.Bool.⇒ (Data.Bool.∧ (llist.LFINITE t) (P t))
                    (P (llist.LCONS h t))))))
    (Data.Bool.∀ (λll1. Data.Bool.⇒ (llist.LFINITE ll1) (P ll1)))

⊦ Data.Bool.∀
    (λm.
       Data.Bool.∀
         (λh.
            Data.Bool.∀
              (λt.
                 llist.LTAKE m (llist.LCONS h t) = Data.Option.NONE ⇔
                 Data.Bool.∃
                   (λn.
                      Data.Bool.∧ (m = Number.Natural.suc n)
                        (llist.LTAKE n t = Data.Option.NONE)))))

⊦ Data.Bool.∧ (Data.Bool.∀ (λf. llist.LMAP f llist.LNIL = llist.LNIL))
    (Data.Bool.∀
       (λf.
          Data.Bool.∀
            (λh.
               Data.Bool.∀
                 (λt.
                    llist.LMAP f (llist.LCONS h t) =
                    llist.LCONS (f h) (llist.LMAP f t)))))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λQ.
            Data.Bool.⇒
              (Data.Bool.∀
                 (λh.
                    Data.Bool.∀
                      (λt.
                         Data.Bool.⇒ (Q (llist.LCONS h t))
                           (Data.Bool.∧ (P h) (Q t)))))
              (Data.Bool.∀ (λll. Data.Bool.⇒ (Q ll) (llist.every P ll)))))

⊦ Data.Bool.∀
    (λn.
       Data.Bool.∀
         (λll.
            llist.LTAKE (Number.Natural.suc n) ll =
            Data.Option.case Data.Option.NONE
              (λl.
                 Data.Option.case Data.Option.NONE
                   (λe.
                      Data.Option.SOME
                        (Data.List.@ l (Data.List.:: e Data.List.[])))
                   (llist.LNTH n ll)) (llist.LTAKE n ll)))

⊦ Data.Bool.∀
    (λLFINITE'.
       Data.Bool.⇒
         (Data.Bool.∧ (LFINITE' llist.LNIL)
            (Data.Bool.∀
               (λh.
                  Data.Bool.∀
                    (λt.
                       Data.Bool.⇒
                         (Data.Bool.∧ (llist.LFINITE t) (LFINITE' t))
                         (LFINITE' (llist.LCONS h t))))))
         (Data.Bool.∀ (λa0. Data.Bool.⇒ (llist.LFINITE a0) (LFINITE' a0))))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∃
         (λg.
            Data.Bool.∧
              (Data.Bool.∀
                 (λx.
                    llist.LHD (g x) = Data.Option.map Data.Pair.snd (f x)))
              (Data.Bool.∀
                 (λx.
                    llist.LTL (g x) =
                    Data.Option.map (Function.∘ g Data.Pair.fst) (f x)))))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∃!
         (λg.
            Data.Bool.∧
              (Data.Bool.∀
                 (λx.
                    llist.LHD (g x) = Data.Option.map Data.Pair.snd (f x)))
              (Data.Bool.∀
                 (λx.
                    llist.LTL (g x) =
                    Data.Option.map (Function.∘ g Data.Pair.fst) (f x)))))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∧
         (Data.Bool.∀
            (λh.
               Data.Bool.∀
                 (λt.
                    Data.Bool.⇒ (P h) (llist.exists P (llist.LCONS h t)))))
         (Data.Bool.∀
            (λh.
               Data.Bool.∀
                 (λt.
                    Data.Bool.⇒ (llist.exists P t)
                      (llist.exists P (llist.LCONS h t))))))

⊦ llist.LFINITE =
  λa0.
    Data.Bool.∀
      (λLFINITE'.
         Data.Bool.⇒
           (Data.Bool.∀
              (λa0.
                 Data.Bool.⇒
                   (Data.Bool.∨ (a0 = llist.LNIL)
                      (Data.Bool.∃
                         (λh.
                            Data.Bool.∃
                              (λt.
                                 Data.Bool.∧ (a0 = llist.LCONS h t)
                                   (LFINITE' t))))) (LFINITE' a0)))
           (LFINITE' a0))

⊦ Data.Bool.∧ (Data.Bool.∀ (λP. llist.LFILTER P llist.LNIL = llist.LNIL))
    (Data.Bool.∀
       (λP.
          Data.Bool.∀
            (λh.
               Data.Bool.∀
                 (λt.
                    llist.LFILTER P (llist.LCONS h t) =
                    if P h then llist.LCONS h (llist.LFILTER P t)
                    else llist.LFILTER P t))))

⊦ Data.Bool.∧ (llist.LUNZIP llist.LNIL = Data.Pair., llist.LNIL llist.LNIL)
    (Data.Bool.∀
       (λx.
          Data.Bool.∀
            (λy.
               Data.Bool.∀
                 (λt.
                    llist.LUNZIP (llist.LCONS (Data.Pair., x y) t) =
                    Data.Bool.let
                      (Data.Pair.uncurry
                         (λll1 ll2.
                            Data.Pair., (llist.LCONS x ll1)
                              (llist.LCONS y ll2))) (llist.LUNZIP t)))))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λa0.
            llist.exists P a0 ⇔
            Data.Bool.∨
              (Data.Bool.∃
                 (λh.
                    Data.Bool.∃
                      (λt. Data.Bool.∧ (a0 = llist.LCONS h t) (P h))))
              (Data.Bool.∃
                 (λh.
                    Data.Bool.∃
                      (λt.
                         Data.Bool.∧ (a0 = llist.LCONS h t)
                           (llist.exists P t))))))

⊦ Data.Bool.∀
    (λlo.
       llist.linear_order_to_list_f lo =
       Data.Bool.let
         (λmin.
            if min = Set.∅ then Data.Option.NONE
            else
              Data.Option.SOME
                (Data.Pair.,
                   (Relation.restrict lo
                      (Set.-
                         (Set.∪ (Relation.domain lo) (Relation.range lo))
                         min)) (Set.choice min)))
         (Relation.minimalElements
            (Set.∪ (Relation.domain lo) (Relation.range lo)) lo))

⊦ Data.Bool.∀
    (λllength_rel'.
       Data.Bool.⇒
         (Data.Bool.∧ (llength_rel' llist.LNIL Number.Numeral.zero)
            (Data.Bool.∀
               (λh.
                  Data.Bool.∀
                    (λn.
                       Data.Bool.∀
                         (λt.
                            Data.Bool.⇒ (llength_rel' t n)
                              (llength_rel' (llist.LCONS h t)
                                 (Number.Natural.suc n)))))))
         (Data.Bool.∀
            (λa0.
               Data.Bool.∀
                 (λa1.
                    Data.Bool.⇒ (llist.llength_rel a0 a1)
                      (llength_rel' a0 a1)))))

⊦ Data.Bool.∧
    (Data.Bool.∀
       (λll. llist.LDROP Number.Numeral.zero ll = Data.Option.SOME ll))
    (Data.Bool.∧
       (Data.Bool.∀
          (λn.
             llist.LDROP (Number.Natural.suc n) llist.LNIL =
             Data.Option.NONE))
       (Data.Bool.∀
          (λn.
             Data.Bool.∀
               (λh.
                  Data.Bool.∀
                    (λt.
                       llist.LDROP (Number.Natural.suc n)
                         (llist.LCONS h t) = llist.LDROP n t)))))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λll.
            llist.LFILTER P ll =
            if Data.Bool.¬ (llist.exists P ll) then llist.LNIL
            else if P (Data.Option.the (llist.LHD ll)) then
              llist.LCONS (Data.Option.the (llist.LHD ll))
                (llist.LFILTER P (Data.Option.the (llist.LTL ll)))
            else llist.LFILTER P (Data.Option.the (llist.LTL ll))))

⊦ Data.Bool.∧ (llist.LFLATTEN llist.LNIL = llist.LNIL)
    (Data.Bool.∧
       (Data.Bool.∀
          (λtl.
             llist.LFLATTEN (llist.LCONS llist.LNIL t) = llist.LFLATTEN t))
       (Data.Bool.∀
          (λh.
             Data.Bool.∀
               (λt.
                  Data.Bool.∀
                    (λtl.
                       llist.LFLATTEN (llist.LCONS (llist.LCONS h t) tl) =
                       llist.LCONS h
                         (llist.LFLATTEN (llist.LCONS t tl)))))))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λexists'.
            Data.Bool.⇒
              (Data.Bool.∧
                 (Data.Bool.∀
                    (λh.
                       Data.Bool.∀
                         (λt.
                            Data.Bool.⇒ (P h)
                              (exists' (llist.LCONS h t)))))
                 (Data.Bool.∀
                    (λh.
                       Data.Bool.∀
                         (λt.
                            Data.Bool.⇒ (exists' t)
                              (exists' (llist.LCONS h t))))))
              (Data.Bool.∀
                 (λa0. Data.Bool.⇒ (llist.exists P a0) (exists' a0)))))

⊦ Data.Bool.∧
    (Data.Bool.∀
       (λll.
          llist.LTAKE Number.Numeral.zero ll =
          Data.Option.SOME Data.List.[]))
    (Data.Bool.∀
       (λn.
          Data.Bool.∀
            (λll.
               llist.LTAKE (Number.Natural.suc n) ll =
               Data.Option.case Data.Option.NONE
                 (λhd.
                    Data.Option.case Data.Option.NONE
                      (λtl. Data.Option.SOME (Data.List.:: hd tl))
                      (llist.LTAKE n (Data.Option.the (llist.LTL ll))))
                 (llist.LHD ll))))

⊦ Data.Bool.∀
    (λa0.
       Data.Bool.∀
         (λa1.
            llist.llength_rel a0 a1 ⇔
            Data.Bool.∨
              (Data.Bool.∧ (a0 = llist.LNIL) (a1 = Number.Numeral.zero))
              (Data.Bool.∃
                 (λh.
                    Data.Bool.∃
                      (λn.
                         Data.Bool.∃
                           (λt.
                              Data.Bool.∧ (a0 = llist.LCONS h t)
                                (Data.Bool.∧ (a1 = Number.Natural.suc n)
                                   (llist.llength_rel t n))))))))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∀
         (λx.
            Data.Bool.∀
              (λv1.
                 Data.Bool.∀
                   (λv2.
                      Data.Bool.∧
                        (Data.Bool.⇒ (f x = Data.Option.NONE)
                           (llist.LUNFOLD f x = llist.LNIL))
                        (Data.Bool.⇒
                           (f x = Data.Option.SOME (Data.Pair., v1 v2))
                           (llist.LUNFOLD f x =
                            llist.LCONS v2 (llist.LUNFOLD f v1)))))))

⊦ Data.Bool.∧
    (Data.Bool.∀ (λn. llist.LNTH n llist.LNIL = Data.Option.NONE))
    (Data.Bool.∧
       (Data.Bool.∀
          (λh.
             Data.Bool.∀
               (λt.
                  llist.LNTH Number.Numeral.zero (llist.LCONS h t) =
                  Data.Option.SOME h)))
       (Data.Bool.∀
          (λn.
             Data.Bool.∀
               (λh.
                  Data.Bool.∀
                    (λt.
                       llist.LNTH (Number.Natural.suc n)
                         (llist.LCONS h t) = llist.LNTH n t)))))

⊦ Data.Bool.∧
    (Data.Bool.∀
       (λll.
          llist.LTAKE Number.Numeral.zero ll =
          Data.Option.SOME Data.List.[]))
    (Data.Bool.∧
       (Data.Bool.∀
          (λn.
             llist.LTAKE (Number.Natural.suc n) llist.LNIL =
             Data.Option.NONE))
       (Data.Bool.∀
          (λn.
             Data.Bool.∀
               (λh.
                  Data.Bool.∀
                    (λt.
                       llist.LTAKE (Number.Natural.suc n)
                         (llist.LCONS h t) =
                       Data.Option.map (Data.List.:: h)
                         (llist.LTAKE n t))))))

⊦ Data.Bool.∀
    (λllength_rel'.
       Data.Bool.⇒
         (Data.Bool.∧ (llength_rel' llist.LNIL Number.Numeral.zero)
            (Data.Bool.∀
               (λh.
                  Data.Bool.∀
                    (λn.
                       Data.Bool.∀
                         (λt.
                            Data.Bool.⇒
                              (Data.Bool.∧ (llist.llength_rel t n)
                                 (llength_rel' t n))
                              (llength_rel' (llist.LCONS h t)
                                 (Number.Natural.suc n)))))))
         (Data.Bool.∀
            (λa0.
               Data.Bool.∀
                 (λa1.
                    Data.Bool.⇒ (llist.llength_rel a0 a1)
                      (llength_rel' a0 a1)))))

⊦ llist.exists =
  λP a0.
    Data.Bool.∀
      (λexists'.
         Data.Bool.⇒
           (Data.Bool.∀
              (λa0.
                 Data.Bool.⇒
                   (Data.Bool.∨
                      (Data.Bool.∃
                         (λh.
                            Data.Bool.∃
                              (λt.
                                 Data.Bool.∧ (a0 = llist.LCONS h t)
                                   (P h))))
                      (Data.Bool.∃
                         (λh.
                            Data.Bool.∃
                              (λt.
                                 Data.Bool.∧ (a0 = llist.LCONS h t)
                                   (exists' t))))) (exists' a0)))
           (exists' a0))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λQ.
            Data.Bool.⇒
              (Data.Bool.∧
                 (Data.Bool.∀
                    (λh.
                       Data.Bool.∀
                         (λt. Data.Bool.⇒ (P h) (Q (llist.LCONS h t)))))
                 (Data.Bool.∀
                    (λh.
                       Data.Bool.∀
                         (λt.
                            Data.Bool.⇒
                              (Data.Bool.∧ (Q t) (llist.exists P t))
                              (Q (llist.LCONS h t))))))
              (Data.Bool.∀ (λll. Data.Bool.⇒ (llist.exists P ll) (Q ll)))))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λexists'.
            Data.Bool.⇒
              (Data.Bool.∧
                 (Data.Bool.∀
                    (λh.
                       Data.Bool.∀
                         (λt.
                            Data.Bool.⇒ (P h)
                              (exists' (llist.LCONS h t)))))
                 (Data.Bool.∀
                    (λh.
                       Data.Bool.∀
                         (λt.
                            Data.Bool.⇒
                              (Data.Bool.∧ (llist.exists P t) (exists' t))
                              (exists' (llist.LCONS h t))))))
              (Data.Bool.∀
                 (λa0. Data.Bool.⇒ (llist.exists P a0) (exists' a0)))))

⊦ Data.Bool.∀
    (λP.
       Data.Bool.∀
         (λQ.
            Data.Bool.⇒
              (Data.Bool.∧
                 (Data.Bool.∀
                    (λh.
                       Data.Bool.∀
                         (λt. Data.Bool.⇒ (Q (llist.LCONS h t)) (P h))))
                 (Data.Bool.∀
                    (λh.
                       Data.Bool.∀
                         (λt.
                            Data.Bool.⇒ (Q (llist.LCONS h t))
                              (Data.Bool.∨ (Q t) (llist.every P t))))))
              (Data.Bool.∀ (λll. Data.Bool.⇒ (Q ll) (llist.every P ll)))))

⊦ Data.Bool.∀
    (λll.
       llist.LFLATTEN ll =
       if llist.every ((=) llist.LNIL) ll then llist.LNIL
       else if Data.Option.the (llist.LHD ll) = llist.LNIL then
         llist.LFLATTEN (Data.Option.the (llist.LTL ll))
       else
         llist.LCONS
           (Data.Option.the (llist.LHD (Data.Option.the (llist.LHD ll))))
           (llist.LFLATTEN
              (llist.LCONS
                 (Data.Option.the
                    (llist.LTL (Data.Option.the (llist.LHD ll))))
                 (Data.Option.the (llist.LTL ll)))))

⊦ Data.Bool.∀
    (λf.
       llist.lrep_ok f ⇔
       Data.Bool.∃
         (λP.
            Data.Bool.∧
              (Data.Bool.∀
                 (λg.
                    Data.Bool.⇒ (P g)
                      (Data.Bool.∨ (g = λn. Data.Option.NONE)
                         (Data.Bool.∃
                            (λh.
                               Data.Bool.∃
                                 (λt.
                                    Data.Bool.∧ (P t)
                                      (g =
                                       λn.
                                         if n = Number.Numeral.zero then
                                           Data.Option.SOME h
                                         else
                                           t
                                             (Number.Natural.- n
                                                (Number.Numeral.bit1
                                                   Number.Numeral.zero)))))))))
              (P f)))

⊦ Data.Bool.∀
    (λf.
       Data.Bool.∀
         (λg.
            Data.Bool.⇒
              (Data.Bool.∀
                 (λx.
                    Data.Bool.∨
                      (Data.Bool.∧ (f x = llist.LNIL) (g x = llist.LNIL))
                      (Data.Bool.∃
                         (λh.
                            Data.Bool.∃
                              (λy.
                                 Data.Bool.∧ (f x = llist.LCONS h (f y))
                                   (g x = llist.LCONS h (g y)))))))
              (Data.Bool.∀ (λx. f x = g x))))

⊦ Data.Bool.∧
    (Data.Bool.∀
       (λl1. llist.LZIP (Data.Pair., l1 llist.LNIL) = llist.LNIL))
    (Data.Bool.∧
       (Data.Bool.∀
          (λl2. llist.LZIP (Data.Pair., llist.LNIL l2) = llist.LNIL))
       (Data.Bool.∀
          (λh1.
             Data.Bool.∀
               (λh2.
                  Data.Bool.∀
                    (λt1.
                       Data.Bool.∀
                         (λt2.
                            llist.LZIP
                              (Data.Pair., (llist.LCONS h1 t1)
                                 (llist.LCONS h2 t2)) =
                            llist.LCONS (Data.Pair., h1 h2)
                              (llist.LZIP (Data.Pair., t1 t2))))))))

⊦ Data.Bool.∀
    (λll1.
       Data.Bool.∀
         (λll2.
            ll1 = ll2 ⇔
            Data.Bool.∃
              (λR.
                 Data.Bool.∧ (R ll1 ll2)
                   (Data.Bool.∀
                      (λll3.
                         Data.Bool.∀
                           (λll4.
                              Data.Bool.⇒ (R ll3 ll4)
                                (Data.Bool.∨
                                   (Data.Bool.∧ (ll3 = llist.LNIL)
                                      (ll4 = llist.LNIL))
                                   (Data.Bool.∧
                                      (llist.LHD ll3 = llist.LHD ll4)
                                      (R (Data.Option.the (llist.LTL ll3))
                                         (Data.Option.the
                                            (llist.LTL ll4)))))))))))

⊦ llist.llength_rel =
  λa0 a1.
    Data.Bool.∀
      (λllength_rel'.
         Data.Bool.⇒
           (Data.Bool.∀
              (λa0.
                 Data.Bool.∀
                   (λa1.
                      Data.Bool.⇒
                        (Data.Bool.∨
                           (Data.Bool.∧ (a0 = llist.LNIL)
                              (a1 = Number.Numeral.zero))
                           (Data.Bool.∃
                              (λh.
                                 Data.Bool.∃
                                   (λn.
                                      Data.Bool.∃
                                        (λt.
                                           Data.Bool.∧
                                             (a0 = llist.LCONS h t)
                                             (Data.Bool.∧
                                                (a1 = Number.Natural.suc n)
                                                (llength_rel' t n)))))))
                        (llength_rel' a0 a1)))) (llength_rel' a0 a1))

⊦ Data.Bool.∀
    (λm.
       Data.Bool.∀
         (λh.
            Data.Bool.∀
              (λt.
                 Data.Bool.∀
                   (λl.
                      llist.LTAKE m (llist.LCONS h t) =
                      Data.Option.SOME l ⇔
                      Data.Bool.∨
                        (Data.Bool.∧ (m = Number.Numeral.zero)
                           (l = Data.List.[]))
                        (Data.Bool.∃
                           (λn.
                              Data.Bool.∃
                                (λl'.
                                   Data.Bool.∧ (m = Number.Natural.suc n)
                                     (Data.Bool.∧
                                        (llist.LTAKE n t =
                                         Data.Option.SOME l')
                                        (l = Data.List.:: h l')))))))))

⊦ Data.Bool.∀
    (λll1.
       Data.Bool.∀
         (λll2.
            ll1 = ll2 ⇔
            Data.Bool.∃
              (λR.
                 Data.Bool.∧ (R ll1 ll2)
                   (Data.Bool.∀
                      (λll3.
                         Data.Bool.∀
                           (λll4.
                              Data.Bool.⇒ (R ll3 ll4)
                                (Data.Bool.∨ (ll3 = ll4)
                                   (Data.Bool.∃
                                      (λh.
                                         Data.Bool.∃
                                           (λt1.
                                              Data.Bool.∃
                                                (λt2.
                                                   Data.Bool.∧
                                                     (ll3 =
                                                      llist.LCONS h t1)
                                                     (Data.Bool.∧
                                                        (ll4 =
                                                         llist.LCONS h t2)
                                                        (R t1
                                                           t2)))))))))))))

⊦ Data.Bool.∧
    (Data.Bool.∀
       (λn.
          Data.Bool.∀
            (λll.
               Data.Bool.⇒ (Data.Bool.¬ (llist.LFINITE ll))
                 (llist.LAPPEND
                    (llist.fromList (Data.Option.the (llist.LTAKE n ll)))
                    (Data.Option.the (llist.LDROP n ll)) = ll))))
    (Data.Bool.∀
       (λn.
          Data.Bool.∀
            (λll.
               Data.Bool.⇒
                 (Data.Bool.∧ (llist.LFINITE ll)
                    (Number.Natural.≤ n
                       (Data.Option.the (llist.LLENGTH ll))))
                 (llist.LAPPEND
                    (llist.fromList (Data.Option.the (llist.LTAKE n ll)))
                    (Data.Option.the (llist.LDROP n ll)) = ll))))

⊦ Data.Bool.∀
    (λll1.
       Data.Bool.∀
         (λll2.
            ll1 = ll2 ⇔
            Data.Bool.∃
              (λR.
                 Data.Bool.∧ (R ll1 ll2)
                   (Data.Bool.∀
                      (λll3.
                         Data.Bool.∀
                           (λll4.
                              Data.Bool.⇒ (R ll3 ll4)
                                (Data.Bool.∨
                                   (Data.Bool.∧ (ll3 = llist.LNIL)
                                      (ll4 = llist.LNIL))
                                   (Data.Bool.∃
                                      (λh.
                                         Data.Bool.∃
                                           (λt1.
                                              Data.Bool.∃
                                                (λt2.
                                                   Data.Bool.∧
                                                     (ll3 =
                                                      llist.LCONS h t1)
                                                     (Data.Bool.∧
                                                        (ll4 =
                                                         llist.LCONS h t2)
                                                        (R t1
                                                           t2)))))))))))))

⊦ Data.Bool.∀
    (λR.
       Data.Bool.∀
         (λf.
            Data.Bool.∀
              (λs.
                 Data.Bool.∀
                   (λll.
                      Data.Bool.⇒
                        (Data.Bool.∧ (R s ll)
                           (Data.Bool.∀
                              (λs.
                                 Data.Bool.∀
                                   (λll.
                                      Data.Bool.⇒ (R s ll)
                                        (Data.Bool.∨
                                           (Data.Bool.∧
                                              (f s = Data.Option.NONE)
                                              (ll = llist.LNIL))
                                           (Data.Bool.∃
                                              (λs'.
                                                 Data.Bool.∃
                                                   (λx.
                                                      Data.Bool.∃
                                                        (λll'.
                                                           Data.Bool.∧
                                                             (f s =
                                                              Data.Option.SOME
                                                                (Data.Pair.,
                                                                   s' x))
                                                             (Data.Bool.∧
                                                                (llist.LHD
                                                                   ll =
                                                                 Data.Option.SOME
                                                                   x)
                                                                (Data.Bool.∧
                                                                   (llist.LTL
                                                                      ll =
                                                                    Data.Option.SOME
                                                                      ll')
                                                                   (R s'
                                                                      ll'))))))))))))
                        (llist.LUNFOLD f s = ll)))))

⊦ Data.Bool.∀
    (λlo.
       Data.Bool.∀
         (λX.
            Data.Bool.⇒
              (Data.Bool.∧ (Relation.linearOrder lo X)
                 (Relation.finitePrefixes lo X))
              (Data.Bool.∃
                 (λll.
                    Data.Bool.∧
                      (X =
                       Set.specification
                         (λx.
                            Data.Pair., x
                              (Data.Bool.∃
                                 (λi.
                                    llist.LNTH i ll =
                                    Data.Option.SOME x))))
                      (Data.Bool.∧
                         (Set.⊆ lo
                            (Set.specification
                               (Data.Pair.uncurry
                                  (λx y.
                                     Data.Pair., (Data.Pair., x y)
                                       (Data.Bool.∃
                                          (λi.
                                             Data.Bool.∃
                                               (λj.
                                                  Data.Bool.∧
                                                    (Number.Natural.≤ i j)
                                                    (Data.Bool.∧
                                                       (llist.LNTH i ll =
                                                        Data.Option.SOME x)
                                                       (llist.LNTH j ll =
                                                        Data.Option.SOME
                                                          y)))))))))
                         (Data.Bool.∀
                            (λi.
                               Data.Bool.∀
                                 (λj.
                                    Data.Bool.∀
                                      (λx.
                                         Data.Bool.⇒
                                           (Data.Bool.∧
                                              (llist.LNTH i ll =
                                               Data.Option.SOME x)
                                              (llist.LNTH j ll =
                                               Data.Option.SOME x))
                                           (i = j))))))))))

Input Type Operators

• →
• bool
• Data
  • List
    • Data.List.list
  • Option
    • Data.Option.option
  • Pair
    • Data.Pair.×
• Number
  • Natural
    • Number.Natural.natural

Input Constants

• =
• Data
  • Bool
    • Data.Bool.∀
    • Data.Bool.∧
    • Data.Bool.⇒
    • Data.Bool.∃
    • Data.Bool.∃!
    • Data.Bool.∨
    • Data.Bool.¬
    • Data.Bool.cond
    • Data.Bool.let
    • Data.Bool.select
    • Data.Bool.F
    • Data.Bool.T
  • List
    • Data.List.::
    • Data.List.@
    • Data.List.[]
    • Data.List.length
  • Option
    • Data.Option.case
    • Data.Option.join
    • Data.Option.map
    • Data.Option.the
    • Data.Option.NONE
    • Data.Option.SOME
  • Pair
    • Data.Pair.,
    • Data.Pair.case
    • Data.Pair.fst
    • Data.Pair.snd
    • Data.Pair.uncurry
• Function
  • Function.id
  • Function.∘
  • Combinator
    • Function.Combinator.c
    • Function.Combinator.s
• HOL4
  • Numeral
    • HOL4.Numeral.iiSUC
  • HOL4.TYPE_DEFINITION
• Number
  • Natural
    • Number.Natural.*
    • Number.Natural.+
    • Number.Natural.-
    • Number.Natural.<
    • Number.Natural.≤
    • Number.Natural.>
    • Number.Natural.≥
    • Number.Natural.even
    • Number.Natural.exp
    • Number.Natural.odd
    • Number.Natural.pre
    • Number.Natural.suc
  • Numeral
    • Number.Numeral.bit1
    • Number.Numeral.bit2
    • Number.Numeral.zero
• Relation
  • Relation.antisymmetric
  • Relation.domain
  • Relation.finitePrefixes
  • Relation.linearOrder
  • Relation.minimalElements
  • Relation.range
  • Relation.restrict
  • Relation.transitive
• Set
  • Set.-
  • Set.∅
  • Set.choice
  • Set.finite
  • Set.in
  • Set.insert
  • Set.⊂
  • Set.singleton
  • Set.specification
  • Set.⊆
  • Set.∪
• While
  • While.least
  • While.while

Assumptions

⊦ Data.Bool.T

⊦ Data.Bool.∀ (λx. x = x)

⊦ Data.Bool.∀ (λt. Data.Bool.⇒ Data.Bool.F t)

⊦ Data.Bool.∀ (λn. Number.Natural.≤ Number.Numeral.zero n)

⊦ Data.Bool.∀ (λs. Set.⊆ s s)

⊦ Data.Bool.¬ (Data.Bool.∧ t (Data.Bool.¬ t))

⊦ Number.Numeral.bit1 Number.Numeral.zero =
  Number.Natural.suc Number.Numeral.zero

⊦ Data.Bool.⇒ (Data.Bool.¬ (Data.Bool.¬ p)) p

⊦ Data.Bool.∀ (λx. Data.Bool.¬ (Set.in x Set.∅))

⊦ Data.Bool.∀ (λx. Function.id x = x)

⊦ Data.Bool.∀ (λt. Data.Bool.∨ t (Data.Bool.¬ t))

⊦ Data.Bool.∀ (λn. Data.Bool.¬ (Number.Natural.< n Number.Numeral.zero))

⊦ Data.Bool.∀
    (λn. Number.Natural.< Number.Numeral.zero (Number.Natural.suc n))

⊦ Data.Bool.¬ = λt. Data.Bool.⇒ t Data.Bool.F

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

⊦ Data.Bool.∀ (λa. Data.Bool.∃ (λx. x = a))

⊦ Data.Bool.∀ (λt. Data.Bool.∀ (λx. t) ⇔ t)

⊦ Data.Bool.∀ (λt. Data.Bool.∃ (λx. t) ⇔ t)

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

⊦ Data.Bool.∀ = λP. P = λx. Data.Bool.T

⊦ Number.Numeral.bit2 Number.Numeral.zero =
  Number.Natural.suc (Number.Numeral.bit1 Number.Numeral.zero)

⊦ Data.Bool.⇒ (Data.Bool.¬ (Data.Bool.⇒ p q)) p

⊦ Data.Bool.∀ (λx. Data.Bool.¬ (Data.Option.NONE = Data.Option.SOME x))

⊦ Data.Bool.∀ (λx. Data.Bool.¬ (Data.Option.SOME x = Data.Option.NONE))

⊦ Data.Bool.∀ (λx. Data.Option.the (Data.Option.SOME x) = x)

⊦ Data.Bool.∀ (λx. x = x ⇔ Data.Bool.T)

⊦ Data.Bool.∀ (λt. Data.Bool.¬ (Data.Bool.¬ t) ⇔ t)