Theory indexedLists

⊢ (∀f a. FOLDRi f a [] = a) ∧
  ∀f a h t. FOLDRi f a (h::t) = f 0 h (FOLDRi (f ∘ SUC) a t)

⊢ (∀f i a. MAPi_ACC f i a [] = REVERSE a) ∧
  ∀f i a h t. MAPi_ACC f i a (h::t) = MAPi_ACC f (i + 1) (f i h::a) t

⊢ (∀f. MAPi f [] = []) ∧ ∀f h t. MAPi f (h::t) = f 0 h::MAPi (f ∘ SUC) t

⊢ (∀i. delN i [] = []) ∧
  ∀i h t. delN i (h::t) = if i = 0 then t else h::delN (i − 1) t

⊢ (∀x. findi x [] = 0) ∧
  ∀x h t. findi x (h::t) = if x = h then 0 else 1 + findi x t

⊢ ∀f l1 l2 n.
    n < LENGTH l1 ∧ n < LENGTH l2 ⇒ (MAP2i f l1 l2)❲n❳ = f n l1❲n❳ l2❲n❳

⊢ ∀f n l. n < LENGTH l ⇒ (MAPi f l)❲n❳ = f n l❲n❳

⊢ ∀l i j. j ≤ i ∧ i + 1 < LENGTH l ⇒ (delN j l)❲i❳ = l❲i + 1❳

⊢ ∀l i j. i < j ∧ j < LENGTH l ⇒ (delN j l)❲i❳ = l❲i❳

⊢ ∀l x. MEM x l ⇒ l❲findi x l❳ = x

⊢ ∀f g a l. FOLDR f a (MAPi g l) = FOLDRi ($o f ∘ g) a l

⊢ ∀f. FOLDRi f a (l1 ⧺ l2) = FOLDRi f (FOLDRi (f ∘ $+ (LENGTH l1)) a l2) l1

⊢ l1 = l2 ⇒
  (∀n e a. n < LENGTH l2 ⇒ MEM e l2 ⇒ f1 n e a = f2 n e a) ⇒
  a1 = a2 ⇒
  FOLDRi f1 a1 l1 = FOLDRi f2 a2 l2

⊢ l1 = l2 ∧ (∀n a. n < LENGTH l2 ⇒ f1 n l2❲n❳ a = f2 n l2❲n❳ a) ∧ a1 = a2 ⇒
  FOLDRi f1 a1 l1 = FOLDRi f2 a2 l2

⊢ ∀f l1 l2. LENGTH (MAP2i f l1 l2) = MIN (LENGTH l1) (LENGTH l2)

⊢ ∀f l. LENGTH (MAPi f l) = LENGTH l

⊢ LIST_RELi R l1 l2 ∧ LIST_RELi (R ∘ $+ (LENGTH l1)) m1 m2 ⇒
  LIST_RELi R (l1 ⧺ m1) (l2 ⧺ m2)

⊢ LIST_RELi R l1 l2 ⇔
  LENGTH l1 = LENGTH l2 ∧ ∀i. i < LENGTH l1 ⇒ R i l1❲i❳ l2❲i❳

⊢ ∀l1 l2. LIST_RELi R l1 l2 ⇒ LENGTH l1 = LENGTH l2

⊢ ∀R a0 a1.
    LIST_RELi R a0 a1 ⇔
    a0 = [] ∧ a1 = [] ∨
    ∃h1 h2 l1 l2.
      a0 = l1 ⧺ [h1] ∧ a1 = l2 ⧺ [h2] ∧ R (LENGTH l1) h1 h2 ∧
      LIST_RELi R l1 l2

⊢ ∀R LIST_RELi'.
    LIST_RELi' [] [] ∧
    (∀h1 h2 l1 l2.
       R (LENGTH l1) h1 h2 ∧ LIST_RELi' l1 l2 ⇒
       LIST_RELi' (l1 ⧺ [h1]) (l2 ⧺ [h2])) ⇒
    ∀a0 a1. LIST_RELi R a0 a1 ⇒ LIST_RELi' a0 a1

⊢ ∀R. LIST_RELi R [] [] ∧
      ∀h1 h2 l1 l2.
        R (LENGTH l1) h1 h2 ∧ LIST_RELi R l1 l2 ⇒
        LIST_RELi R (l1 ⧺ [h1]) (l2 ⧺ [h2])

⊢ ∀R LIST_RELi'.
    LIST_RELi' [] [] ∧
    (∀h1 h2 l1 l2.
       R (LENGTH l1) h1 h2 ∧ LIST_RELi R l1 l2 ∧ LIST_RELi' l1 l2 ⇒
       LIST_RELi' (l1 ⧺ [h1]) (l2 ⧺ [h2])) ⇒
    ∀a0 a1. LIST_RELi R a0 a1 ⇒ LIST_RELi' a0 a1

⊢ (LIST_RELi R [] x ⇔ x = []) ∧
  (LIST_RELi R (h::t) l ⇔
   ∃h' t'. l = h'::t' ∧ R 0 h h' ∧ LIST_RELi (R ∘ SUC) t t')

⊢ MAP2i f l1 [] = []

⊢ MAP2i f l1 l2 = indexedLists$MAP2ia f 0 l1 l2

⊢ (∀v0 f. MAP2i f [] v0 = []) ∧ (∀v6 v5 f. MAP2i f (v5::v6) [] = []) ∧
  ∀t2 t1 h2 h1 f.
    MAP2i f (h1::t1) (h2::t2) = f 0 h1 h2::MAP2i (f ∘ SUC) t1 t2

⊢ ∀P. (∀f v0. P f [] v0) ∧ (∀f v5 v6. P f (v5::v6) []) ∧
      (∀f h1 t1 h2 t2. P (f ∘ SUC) t1 t2 ⇒ P f (h1::t1) (h2::t2)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ indexedLists$MAP2ia f i l1 [] = []

⊢ (∀v0 i f. indexedLists$MAP2ia f i [] v0 = []) ∧
  (∀v8 v7 i f. indexedLists$MAP2ia f i (v7::v8) [] = []) ∧
  ∀t2 t1 i h2 h1 f.
    indexedLists$MAP2ia f i (h1::t1) (h2::t2) =
    f i h1 h2::indexedLists$MAP2ia f (i + 1) t1 t2

⊢ ∀P. (∀f i v0. P f i [] v0) ∧ (∀f i v7 v8. P f i (v7::v8) []) ∧
      (∀f i h1 t1 h2 t2. P f (i + 1) t1 t2 ⇒ P f i (h1::t1) (h2::t2)) ⇒
      ∀v v1 v2 v3. P v v1 v2 v3

⊢ ∀f g l. MAP f (MAPi g l) = MAPi ($o f ∘ g) l

⊢ MAPi_ACC f n a l = REVERSE a ⧺ MAPi (f ∘ $+ n) l

⊢ ∀l1 l2 f. MAPi f (l1 ⧺ l2) = MAPi f l1 ⧺ MAPi (f ∘ $+ (LENGTH l1)) l2

⊢ ∀l1 l2 f1 f2.
    l1 = l2 ∧ (∀x n. MEM x l2 ⇒ f1 n x = f2 n x) ⇒ MAPi f1 l1 = MAPi f2 l2

⊢ l1 = l2 ⇒
  (∀x n. x = l2❲n❳ ⇒ n < LENGTH l2 ⇒ f1 n x = f2 n x) ⇒
  MAPi f1 l1 = MAPi f2 l2

⊢ ∀l. MAPi (λi x. f x) l = MAP f l

⊢ ∀l f. MAPi f l = GENLIST (S f (flip EL l)) (LENGTH l)

⊢ MAPi f l = MAPi_ACC f 0 [] l

⊢ ∀x f l. MEM x (MAPi f l) ⇔ ∃n. n < LENGTH l ∧ x = f n l❲n❳

⊢ MEM x l ⇒ findi x l < LENGTH l

⊢ ∀l i. i < LENGTH l ⇒ LENGTH (delN i l) = LENGTH l − 1

⊢ ∀l1 l2 x.
    findi x (l1 ⧺ l2) =
    if MEM x l1 then findi x l1 else LENGTH l1 + findi x l2

⊢ ∀l n. n < LENGTH l ∧ ALL_DISTINCT l ⇒ findi l❲n❳ l = n

⊢ ∀ls x n.
    ALL_DISTINCT ls ∧ MEM x ls ∧ n < LENGTH ls ⇒
    (x = ls❲n❳ ⇔ findi x ls = n)

⊢ ∀x h t. findi x (h::t) = if x = h then 0 else 1 + findi x t

⊢ ∀x. findi x [] = 0

⊢ ∀ls x. ¬MEM x ls ⇒ findi x ls = LENGTH ls

⊢ (fupdLast f x = [] ⇔ x = []) ∧ ([] = fupdLast f x ⇔ x = [])

⊢ fupdLast f l = if l = [] then [] else FRONT l ⧺ [f (LAST l)]

⊢ (∀f. fupdLast f [] = []) ∧ (∀h f. fupdLast f [h] = [f h]) ∧
  ∀v5 v4 h f. fupdLast f (h::v4::v5) = h::fupdLast f (v4::v5)

⊢ ∀P. (∀f. P f []) ∧ (∀f h. P f [h]) ∧
      (∀f h v4 v5. P f (v4::v5) ⇒ P f (h::v4::v5)) ⇒
      ∀v v1. P v v1