Theory ind_type

⊢ ind_type$BOTTOM = mk_rec ind_type$ZBOT

⊢ ∀c i r.
    ind_type$CONSTR c i r =
    mk_rec (ind_type$ZCONSTR c i (λn. dest_rec (r n)))

⊢ (∀a f. ind_type$FCONS a f 0 = a) ∧
  ∀a f n. ind_type$FCONS a f (SUC n) = f n

⊢ ∀n. ind_type$FNIL n = ARB

⊢ ∀a. ind_type$INJA a = (λn b. b = a)

⊢ ∀f. ind_type$INJF f = (λn. f (nfst n) (nsnd n))

⊢ ∀m. ind_type$INJN m = (λn a. n = m)

⊢ ∀f1 f2.
    ind_type$INJP f1 f2 =
    (λn a. if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a)

⊢ ∀f g. ind_type$ISO f g ⇔ (∀x. f (g x) = x) ∧ ∀y. g (f y) = y

⊢ ∀b x. ind_type$NUMSUM b x = if b then SUC (2 * x) else 2 * x

⊢ ∀x y.
    (NUMLEFT (ind_type$NUMSUM x y) ⇔ x) ∧
    NUMRIGHT (ind_type$NUMSUM x y) = y

⊢ ind_type$ZBOT = ind_type$INJP (ind_type$INJN 0) (@z. T)

⊢ ∀c i r.
    ind_type$ZCONSTR c i r =
    ind_type$INJP (ind_type$INJN (SUC c))
      (ind_type$INJP (ind_type$INJA i) (ind_type$INJF r))

⊢ ∃rep. TYPE_DEFINITION ZRECSPACE rep

⊢ (∀a. mk_rec (dest_rec a) = a) ∧ ∀r. ZRECSPACE r ⇔ dest_rec (mk_rec r) = r

⊢ ∀c i r. ind_type$CONSTR c i r ≠ ind_type$BOTTOM

⊢ ∀P. P ind_type$BOTTOM ∧
      (∀c i r. (∀n. P (r n)) ⇒ P (ind_type$CONSTR c i r)) ⇒
      ∀x. P x

⊢ ∀c1 i1 r1 c2 i2 r2.
    ind_type$CONSTR c1 i1 r1 = ind_type$CONSTR c2 i2 r2 ⇔
    c1 = c2 ∧ i1 = i2 ∧ r1 = r2

⊢ ∀Fn. ∃f. ∀c i r. f (ind_type$CONSTR c i r) = Fn c i r (λn. f (r n))

⊢ ∀x y. dest_rec x = dest_rec y ⇔ x = y

⊢ ind_type$FCONS a f n = if n = 0 then a else f (n − 1)

⊢ ∀a1 a2. ind_type$INJA a1 = ind_type$INJA a2 ⇔ a1 = a2

⊢ ∀f1 f2. ind_type$INJF f1 = ind_type$INJF f2 ⇔ f1 = f2

⊢ ∀n1 n2. ind_type$INJN n1 = ind_type$INJN n2 ⇔ n1 = n2

⊢ ∀f1 f1' f2 f2'.
    ind_type$INJP f1 f2 = ind_type$INJP f1' f2' ⇔ f1 = f1' ∧ f2 = f2'

⊢ ∀P. (∀x1 y1 x2 y2. P x1 y1 = P x2 y2 ⇔ x1 = x2 ∧ y1 = y2) ⇒
      ∃X Y. ∀x y. X (P x y) = x ∧ Y (P x y) = y

⊢ ind_type$ISO f f' ∧ ind_type$ISO g g' ⇒
  ind_type$ISO (λh a'. g (h (f' a'))) (λh a. g' (h (f a)))

⊢ ind_type$ISO (λx. x) (λx. x)

⊢ ind_type$ISO f g ⇒
  (∀P. (∀x. P x) ⇔ ∀x. P (g x)) ∧ (∀P. (∃x. P x) ⇔ ∃x. P (g x)) ∧
  ∀a b. a = g b ⇔ f a = b

⊢ ∀x y. mk_rec x = mk_rec y ⇒ ZRECSPACE x ∧ ZRECSPACE y ⇒ x = y

⊢ ∀b1 x1 b2 x2.
    ind_type$NUMSUM b1 x1 = ind_type$NUMSUM b2 x2 ⇔ (b1 ⇔ b2) ∧ x1 = x2

⊢ ∀c i r. ind_type$ZCONSTR c i r ≠ ind_type$ZBOT

⊢ ∀a0.
    ZRECSPACE a0 ⇔
    a0 = ind_type$ZBOT ∨
    ∃c i r. a0 = ind_type$ZCONSTR c i r ∧ ∀n. ZRECSPACE (r n)

⊢ ∀ZRECSPACE'.
    ZRECSPACE' ind_type$ZBOT ∧
    (∀c i r. (∀n. ZRECSPACE' (r n)) ⇒ ZRECSPACE' (ind_type$ZCONSTR c i r)) ⇒
    ∀a0. ZRECSPACE a0 ⇒ ZRECSPACE' a0

⊢ ZRECSPACE ind_type$ZBOT ∧
  ∀c i r. (∀n. ZRECSPACE (r n)) ⇒ ZRECSPACE (ind_type$ZCONSTR c i r)

⊢ ∀ZRECSPACE'.
    ZRECSPACE' ind_type$ZBOT ∧
    (∀c i r.
       (∀n. ZRECSPACE (r n) ∧ ZRECSPACE' (r n)) ⇒
       ZRECSPACE' (ind_type$ZCONSTR c i r)) ⇒
    ∀a0. ZRECSPACE a0 ⇒ ZRECSPACE' a0