Theory fcp

⊢ $FCP = (λg. @f. ∀i. i < dimindex (:β) ⇒ f ' i = g i)

⊢ ∀a b.
    FCP_CONCAT a b =
    FCP i. if i < dimindex (:γ) then b ' i else a ' (i − dimindex (:γ))

⊢ ∀h v. FCP_CONS h v = (0 :+ h) (FCP i. v ' (PRE i))

⊢ ∀P v. FCP_EVERY P v ⇔ ∀i. dimindex (:α) ≤ i ∨ P (v ' i)

⊢ ∀P v. FCP_EXISTS P v ⇔ ∃i. i < dimindex (:α) ∧ P (v ' i)

⊢ ∀f i v. FCP_FOLD f i v = FOLDL f i (V2L v)

⊢ ∀v. FCP_FST v = FCP i. v ' (i + dimindex (:γ))

⊢ ∀v. FCP_HD v = v ' 0

⊢ ∀f v. FCP_MAP f v = FCP i. f (v ' i)

⊢ ∀v. FCP_SND v = FCP i. v ' i

⊢ ∀v. FCP_TL v = FCP i. v ' (SUC i)

⊢ ∀a b. (a :+ b) = (λm. FCP c. if a = c then b else m ' c)

⊢ ∀a b. FCP_ZIP a b = FCP i. (a ' i,b ' i)

⊢ ∀L. L2V L = FCP i. L❲i❳

⊢ ∀v. V2L v = GENLIST ($' v) (dimindex (:β))

⊢ ∀f. bit0MAP f = bit0_ABS ∘ SUM_MAP f f ∘ bit0_REP

⊢ bit0REL =
  (λR x y.
     ∃z. (∀p. p ∈ bit0SET z ⇒ R (FST p) (SND p)) ∧ bit0MAP FST z = x ∧
         bit0MAP SND z = y)

⊢ bit0SET = S ($UNION ∘ BIMG $= ∘ setL) (BIMG $= ∘ setR) ∘ bit0_REP

⊢ (∀a. bit0_ABS (bit0_REP a) = a) ∧
  ∀r. (λx. T) r ⇔ bit0_REP (bit0_ABS r) = r

⊢ bit0_CONS = bit0_ABS

⊢ ∃rep. TYPE_DEFINITION (λx. T) rep

⊢ (∀a0 f f0. bit0_CASE (BIT0A a0) f f0 = f a0) ∧
  ∀a0 f f0. bit0_CASE (BIT0B a0) f f0 = f0 a0

⊢ (∀f0 a0. bit0_size f0 (BIT0A a0) = 1 + f0 a0) ∧
  ∀f0 a0. bit0_size f0 (BIT0B a0) = 1 + f0 a0

⊢ ∀f. bit1MAP f = bit1_ABS ∘ SUM_MAP f (SUM_MAP f I) ∘ bit1_REP

⊢ bit1REL =
  (λR x y.
     ∃z. (∀p. p ∈ bit1SET z ⇒ R (FST p) (SND p)) ∧ bit1MAP FST z = x ∧
         bit1MAP SND z = y)

⊢ bit1SET =
  S ($UNION ∘ BIMG $= ∘ setL)
    (BIMG (S ($UNION ∘ BIMG $= ∘ setL) (BIMG (K ∅) ∘ setR)) ∘ setR) ∘
  bit1_REP

⊢ (∀a. bit1_ABS (bit1_REP a) = a) ∧
  ∀r. (λx. T) r ⇔ bit1_REP (bit1_ABS r) = r

⊢ bit1_CONS = bit1_ABS

⊢ ∃rep. TYPE_DEFINITION (λx. T) rep

⊢ (∀a0 f f0 v. bit1_CASE (BIT1A a0) f f0 v = f a0) ∧
  (∀a0 f f0 v. bit1_CASE (BIT1B a0) f f0 v = f0 a0) ∧
  ∀f f0 v. bit1_CASE BIT1C f f0 v = v

⊢ (∀f0 a0. bit1_size f0 (BIT1A a0) = 1 + f0 a0) ∧
  (∀f0 a0. bit1_size f0 (BIT1B a0) = 1 + f0 a0) ∧
  ∀f0. bit1_size f0 BIT1C = 0

⊢ ∃rep. TYPE_DEFINITION (λf. T) rep

⊢ (∀a. mk_cart (dest_cart a) = a) ∧
  ∀r. (λf. T) r ⇔ dest_cart (mk_cart r) = r

⊢ dimindex (:α) = if FINITE 𝕌(:α) then CARD 𝕌(:α) else 1

⊢ ∀h f. fcp_CASE (mk_cart h) f = f h

⊢ ∀x i. x ' i = dest_cart x (finite_index i)

⊢ ∃rep. TYPE_DEFINITION (λx. x = ARB ∨ FINITE 𝕌(:α)) rep

⊢ (∀a. mk_finite_image (dest_finite_image a) = a) ∧
  ∀r. (λx. x = ARB ∨ FINITE 𝕌(:α)) r ⇔
      dest_finite_image (mk_finite_image r) = r

⊢ finite_index = @f. ∀x. ∃!n. n < dimindex (:α) ∧ f n = x

⊢ ∀m a. (a :+ m ' a) m = m

⊢ ∀P. FINITE 𝕌(:'N) ∧ (∀i. i < dimindex (:'N) ⇒ FINITE {x | P i x}) ⇒
      CARD {v | (∀i. i < dimindex (:'N) ⇒ P i (v ' i))} =
      nproduct {0 .. dimindex (:'N) − 1} (λi. CARD {x | P i x})

⊢ FINITE 𝕌(:α) ∧ FINITE 𝕌(:'N) ⇒
  CARD 𝕌(:α['N]) = CARD 𝕌(:α) ** dimindex (:'N)

⊢ ∀x y. x = y ⇔ ∀i. i < dimindex (:β) ⇒ x ' i = y ' i

⊢ ∀b x y. (if b then x else y) ' i = if b then x ' i else y ' i

⊢ 1 ≤ dimindex (:α)

⊢ 0 < dimindex (:α)

⊢ dimindex (:α) ≠ 0

⊢ ∀i v. i < dimindex (:β) ⇒ (V2L v)❲i❳ = v ' i

⊢ ∀m a w b.
    (a :+ w) m ' b =
    if b < dimindex (:β) then if a = b then w else m ' b
    else FAIL $' $var$(index out of range) ((a :+ w) m) b

⊢ ∀i. i < dimindex (:β) ⇒ $FCP g ' i = g i

⊢ ∀a b c d.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ∧ FCP_CONCAT a b = FCP_CONCAT c d ⇒
    a = c ∧ b = d

⊢ ∀x. FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒ FCP_CONCAT (FCP_FST x) (FCP_SND x) = x

⊢ ∀a b.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    FCP_FST (FCP_CONCAT a b) = a ∧ FCP_SND (FCP_CONCAT a b) = b

⊢ ∀a v. FCP_CONS a v = L2V (a::V2L v)

⊢ ∀g. (FCP i. g ' i) = g

⊢ ∀P v. FCP_EVERY P v ⇔ EVERY P (V2L v)

⊢ ∀P v. FCP_EXISTS P v ⇔ EXISTS P (V2L v)

⊢ ∀v. FCP_HD v = HD (V2L v)

⊢ ∀f v. FCP_MAP f v = L2V (MAP f (V2L v))

⊢ ∀v. 1 < dimindex (:β) ∧ dimindex (:γ) = dimindex (:β) − 1 ⇒
      FCP_TL v = L2V (TL (V2L v))

⊢ ∀f g. (∀i. i < dimindex (:β) ⇒ f ' i = g i) ⇔ $FCP g = f

⊢ ∀m a b c d. a ≠ b ⇒ (a :+ c) ((b :+ d) m) = (b :+ d) ((a :+ c) m)

⊢ ∀m a b c. (a :+ c) ((a :+ b) m) = (a :+ c) m

⊢ ∀m a v. m ' a = v ⇒ (a :+ v) m = m

⊢ FINITE 𝕌(:α) ∧ FINITE 𝕌(:'N) ⇒ FINITE 𝕌(:α['N])

⊢ ∀P m.
    FINITE 𝕌(:'N) ∧ (∀i. i < dimindex (:'N) ⇒ {x | P i x} HAS_SIZE m i) ⇒
    {v | ∀i. i < dimindex (:'N) ⇒ P i (v ' i)} HAS_SIZE
    nproduct {0 .. dimindex (:'N) − 1} m

⊢ ∀m. 𝕌(:α) HAS_SIZE m ∧ FINITE 𝕌(:'N) ⇒
      𝕌(:α['N]) HAS_SIZE m ** dimindex (:'N)

⊢ ∀v. LENGTH (V2L v) = dimindex (:β)

⊢ INFINITE 𝕌(:α) ⇒ dimindex (:α) = 1

⊢ ∀v. ¬NULL (V2L v)

⊢ ∀i a. i < dimindex (:β) ⇒ L2V a ' i = a❲i❳

⊢ ∀i a. i < dimindex (:β) ⇒ FCP_TL a ' i = a ' (SUC i)

⊢ ∀x. dimindex (:β) = LENGTH x ⇒ V2L (L2V x) = x

⊢ (∀a0 a0'. BIT0A a0 = BIT0A a0' ⇔ a0 = a0') ∧
  ∀a0 a0'. BIT0B a0 = BIT0B a0' ⇔ a0 = a0'

⊢ ∀f0 f1. ∃h. (∀a0. h (BIT0A a0) = f0 a0) ∧ ∀a0. h (BIT0B a0) = f1 a0

⊢ ∀f g x. (∀a. a ∈ bit0SET x ⇒ f a = g a) ⇒ bit0MAP f x = bit0MAP g x

⊢ bit0MAP I = I

⊢ ∀f x. bit0SET (bit0MAP f x) = IMAGE f (bit0SET x)

⊢ bit0MAP g ∘ bit0MAP f = bit0MAP (g ∘ f)

⊢ ∀x. cardleq (bit0SET x) 𝕌(:num)

⊢ ∀M M' f f0.
    M = M' ∧ (∀a0. M' = BIT0A a0 ⇒ f a0 = f' a0) ∧
    (∀a0. M' = BIT0B a0 ⇒ f0 a0 = f0' a0) ⇒
    bit0_CASE M f f0 = bit0_CASE M' f' f0'

⊢ bit0_CASE x f f0 = v ⇔
  (∃a. x = BIT0A a ∧ f a = v) ∨ ∃a. x = BIT0B a ∧ f0 a = v

⊢ ∀a0' a0. BIT0A a0 ≠ BIT0B a0'

⊢ ∀P. (∀a. P (BIT0A a)) ∧ (∀a. P (BIT0B a)) ⇒ ∀b. P b

⊢ ∀a. a ∈ bit0SET ((λa. bit0_ABS ((λa. INL a) a)) a)

⊢ ∀bb. (∃a. bb = BIT0A a) ∨ ∃a. bb = BIT0B a

⊢ ∀a. bit0SET ((λa. bit0_ABS ((λa. (K ∘ INL) a ARB) a)) a) ⊆ {a}

⊢ (∀a0 a0'. BIT1A a0 = BIT1A a0' ⇔ a0 = a0') ∧
  ∀a0 a0'. BIT1B a0 = BIT1B a0' ⇔ a0 = a0'

⊢ ∀f0 f1 f2. ∃h.
    (∀a0. h (BIT1A a0) = f0 a0) ∧ (∀a0. h (BIT1B a0) = f1 a0) ∧
    h BIT1C = f2

⊢ ∀f g x. (∀a. a ∈ bit1SET x ⇒ f a = g a) ⇒ bit1MAP f x = bit1MAP g x

⊢ bit1MAP I = I

⊢ ∀f x. bit1SET (bit1MAP f x) = IMAGE f (bit1SET x)

⊢ bit1MAP g ∘ bit1MAP f = bit1MAP (g ∘ f)

⊢ ∀x. cardleq (bit1SET x) 𝕌(:num)

⊢ ∀M M' f f0 v.
    M = M' ∧ (∀a0. M' = BIT1A a0 ⇒ f a0 = f' a0) ∧
    (∀a0. M' = BIT1B a0 ⇒ f0 a0 = f0' a0) ∧ (M' = BIT1C ⇒ v = v') ⇒
    bit1_CASE M f f0 v = bit1_CASE M' f' f0' v'

⊢ bit1_CASE x f f0 v = v' ⇔
  (∃a. x = BIT1A a ∧ f a = v') ∨ (∃a. x = BIT1B a ∧ f0 a = v') ∨
  x = BIT1C ∧ v = v'

⊢ (∀a0' a0. BIT1A a0 ≠ BIT1B a0') ∧ (∀a0. BIT1A a0 ≠ BIT1C) ∧
  ∀a0. BIT1B a0 ≠ BIT1C

⊢ ∀P. (∀a. P (BIT1A a)) ∧ (∀a. P (BIT1B a)) ∧ P BIT1C ⇒ ∀b. P b

⊢ ∀a. a ∈ bit1SET ((λa. bit1_ABS ((λa. INL a) a)) a)

⊢ ∀bb. (∃a. bb = BIT1A a) ∨ (∃a. bb = BIT1B a) ∨ bb = BIT1C

⊢ ∀a. bit1SET ((λa. bit1_ABS ((λa. K INR ARB (K INR ARB ARB)) a)) a) ⊆ ∅

⊢ FINITE 𝕌(:α) ⇒ CARD 𝕌(:α) = dimindex (:α)

⊢ DATATYPE (bit0 BIT0A BIT0B)

⊢ DATATYPE (bit1 BIT1A BIT1B BIT1C)

⊢ ∀f. ∃g. ∀h. g (mk_cart h) = f h

⊢ ∀P. (∀f. P (mk_cart f)) ⇒ ∀a. P a

⊢ ∀a b f. (x :+ y) ($FCP f) = FCP c. if x = c then y else f c

⊢ FINITE 𝕌(:α bit0) ⇔ FINITE 𝕌(:α)

⊢ FINITE 𝕌(:α bit1) ⇔ FINITE 𝕌(:α)

⊢ FINITE 𝕌(:unit)

⊢ FINITE 𝕌(:α + β) ⇔ FINITE 𝕌(:α) ∧ FINITE 𝕌(:β)

⊢ dimindex (:α bit0) = if FINITE 𝕌(:α) then 2 * dimindex (:α) else 1

⊢ dimindex (:α bit1) = if FINITE 𝕌(:α) then 2 * dimindex (:α) + 1 else 1

⊢ ∀f n.
    $FCP f ' n =
    if n < dimindex (:β) then f n
    else FAIL $' $var$(FCP out of bounds) ($FCP f) n

⊢ dimindex (:unit) = 1

⊢ dimindex (:α + β) =
  if FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) then dimindex (:α) + dimindex (:β) else 1