Theory nlist

⊢ listOfN = nlistrec [] (λh tn t. h::t)

⊢ ∀h t. ncons h t = h ⊗ t + 1

⊢ ∀n nlist. nel n nlist = nhd (ndrop n nlist)

⊢ nfront = nlistrec 0 (λh tn rn. if tn = 0 then 0 else ncons h rn)

⊢ ∀nl. nhd nl = nfst (nl − 1)

⊢ nlast = nlistrec 0 (λh tn rn. if tn = 0 then h else rn)

⊢ nlist_of [] = 0 ∧ ∀h t. nlist_of (h::t) = ncons h (nlist_of t)

⊢ ∀nlist. ntl nlist = nsnd (nlist − 1)

⊢ ∀t. t ≠ 0 ⇒ nlen (nfront t) = nlen t − 1

⊢ ∀l e. MEM e (listOfN l) ⇒ e < l

⊢ listOfN n = h::t ⇔ ∃tn. n = ncons h tn ∧ listOfN tn = t

⊢ (listOfN l = [] ⇔ l = 0) ∧ ([] = listOfN l ⇔ l = 0)

⊢ ∀l1 l2. listOfN l1 = listOfN l2 ⇔ l1 = l2

⊢ ∀l. ∃n. listOfN n = l

⊢ listOfN (ncons h t) = h::listOfN t

⊢ ∀l. listOfN (nlist_of l) = l

⊢ listOfN 0 = []

⊢ h < ncons h t

⊢ t < ncons h t

⊢ ∀l1 l2. ndrop (nlen l1) (napp l1 l2) = l2

⊢ ∀l. l < napp l (ncons x 0)

⊢ napp l1 (ncons l 0) = ncons x 0 ⇔ l1 = 0 ∧ x = l

⊢ ncons x y = ncons h t ⇔ x = h ∧ y = t

⊢ ∀l. l ≠ 0 ⇒ ncons (nhd l) (ntl l) = l

⊢ ncons x y ≠ 0

⊢ nlen l = 1 ⇔ ∃n. l = ncons n 0

⊢ ∀l n. ndrop (SUC n) l = ntl (ndrop n l)

⊢ m ≠ 0 ⇒ ndrop m (ncons x 0) = 0

⊢ nel 0 (ncons h t) = h

⊢ ∀n h t. nel (SUC n) (ncons h t) = nel n t

⊢ ∀l i. i < nlen l ⇒ (listOfN l)❲i❳ = nel i l

⊢ ∀l1 l2.
    l1 = l2 ⇔ nlen l1 = nlen l2 ∧ ∀m. m < nlen l1 ⇒ nel m l1 = nel m l2

⊢ ∀l1 l2. n < nlen l1 ⇒ nel n (napp l1 l2) = nel n l1

⊢ ∀y n x. nlen x ≤ n ⇒ nel n (napp x y) = nel (n − nlen x) y

⊢ 0 < n ⇒ nel n (ncons h t) = nel (n − 1) t

⊢ ∀t. m < nlen (nfront t) ⇒ nel m (nfront t) = nel m t

⊢ nel 0 l = nhd l

⊢ nel x 0 = 0

⊢ ∀pfx. nfront (napp pfx (ncons e 0)) = pfx

⊢ nfront 0 = 0

⊢ nfront (ncons x 0) = 0

⊢ nfront 0 = 0 ∧
  nfront (ncons h t) = if t = 0 then 0 else ncons h (nfront t)

⊢ nhd 0 = 0

⊢ ∀l1 l2. l1 ≠ 0 ⇒ nhd (napp l1 l2) = nhd l1

⊢ ∀l. l ≠ 0 ∧ ntl l ≠ 0 ⇒ nhd (nfront l) = nhd l

⊢ nhd (ncons h t) = h

⊢ ∀l1 l2. l2 ≠ 0 ⇒ nlast (napp l1 l2) = nlast l2

⊢ nlast (ncons h tn) = if tn = 0 then h else nlast tn

⊢ ∀l. nlast l = nel (nlen l − 1) l

⊢ nlast 0 = 0

⊢ ∀n. n = 0 ∨ ∃h t. n = ncons h t

⊢ ∀P. P 0 ∧ (∀h t. P t ⇒ P (ncons h t)) ⇒ ∀n. P n

⊢ ∀l. nlist_of (listOfN l) = l

⊢ (nlist_of l = 0 ⇔ l = []) ∧ (0 = nlist_of l ⇔ l = [])

⊢ ∀n1 n2. nlist_of n1 = nlist_of n2 ⇔ n1 = n2

⊢ ∀l. ∃n. nlist_of n = l

⊢ ∀n l f.
    nlistrec n f l =
    if l = 0 then n
    else f (nfst (l − 1)) (nsnd (l − 1)) (nlistrec n f (nsnd (l − 1)))

⊢ ∀P. (∀n f l. (l ≠ 0 ⇒ P n f (nsnd (l − 1))) ⇒ P n f l) ⇒
      ∀v v1 v2. P v v1 v2

⊢ nlistrec n f 0 = n ∧ nlistrec n f (ncons h t) = f h t (nlistrec n f t)

⊢ ∀t. t = 0 ∨ ∃f l. t = napp f (ncons l 0)

⊢ ∀l m. ntl (nlist_of (DROP m l)) = ndrop m (ntl (nlist_of l))

⊢ ∀n. ntl n ≤ n

⊢ 0 < n ⇒ ntl n < n

⊢ ∀l. ntl (ndrop n l) = ndrop n (ntl l)

⊢ ∀n. n ≠ 0 ⇒ ntl n < n

⊢ ntl (ncons h t) = t

⊢ ntl 0 = 0

⊢ ntl l = 0 ⇔ l = 0 ∨ ∃x. l = ncons x 0