Theory bnfPrelims

⊢ optSET NONE = ∅ ∧ ∀x. optSET (SOME x) = {x}

⊢ BIGUNION ∘ IMAGE (IMAGE f ∘ g) = IMAGE f ∘ BIGUNION ∘ IMAGE g

⊢ BIGUNION ∘ IMAGE (IMAGE f ∘ g) ∘ h = IMAGE f ∘ BIGUNION ∘ IMAGE g ∘ h

⊢ BIMG $= = I

⊢ BIGUNION ∘ IMAGE $= ∘ f = f

⊢ BIMG (λx. IMAGE f (g x)) A = IMAGE f (BIMG g A)

⊢ BIMG (IMAGE f ∘ g) = IMAGE f ∘ BIMG g

⊢ BIMG (K ∅) = K ∅

⊢ ∀sA stA x y f g.
    (∀a. a ∈ (BIMG sA ∘ stA) x ⇒ f a = g a) ∧ y ∈ stA x ⇒
    ∀a. a ∈ sA y ⇒ f a = g a

⊢ ∀stB stA sB sA mp h f.
    stB ∘ mp = IMAGE h ∘ stA ∧ sB ∘ h = IMAGE f ∘ sA ⇒
    (BIMG sB ∘ stB) ∘ mp = IMAGE f ∘ BIMG sA ∘ stA

⊢ ∀B g st.
    INFINITE B ∧ (∀y. g y ≼ B) ∧ (∀x. st x ≼ B) ⇒ ∀x. (BIMG g ∘ st) x ≼ B

⊢ ∀s st x t v. t ∈ st x ∧ v ∈ s t ⇒ v ∈ (BIMG s ∘ st) x

⊢ ∀s st x V W. st x ⊆ V ∧ (∀w. w ∈ V ⇒ s w ⊆ W) ⇒ (BIMG s ∘ st) x ⊆ W

⊢ ∀s t. s =~ t ⇒ s ≼ t

⊢ ∀s t. INFINITE s ∧ s ≼ t ⇒ INFINITE t

⊢ ∀s W w. w ∈ ∅ ⇒ s w ⊆ W

⊢ ∀B. B ≠ ∅ ⇒ ∀x. $= x ≼ B

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

⊢ ∀v. v ∈ $= v

⊢ $= x = {x}

⊢ ∀a. $= a ⊆ {a}

⊢ ∀f. $= ∘ f = IMAGE f ∘ $=

⊢ BIGUNION (IMAGE (IMAGE f ∘ h) A) = IMAGE f (BIGUNION (IMAGE h A))

⊢ (f ∘ IMAGE g) ∘ IMAGE h = f ∘ IMAGE (g ∘ h)

⊢ f ∘ IMAGE g ∘ IMAGE h = f ∘ IMAGE (g ∘ h)

⊢ IMAGE g ∘ IMAGE h ∘ f = IMAGE (g ∘ h) ∘ f

⊢ IMAGE (K ∅) A ≼ B ⇔ A = ∅ ∨ B ≠ ∅

⊢ IMAGE f ∘ $= = $= ∘ f

⊢ ∀B. INFINITE B ⇒ B ≠ ∅

⊢ INFINITE 𝕌(:num + α)

⊢ x ∈ $= y ⇔ x = y

⊢ ∀B x. K ∅ x ≼ B

⊢ ∀W x. K ∅ x ⊆ W

⊢ ∀f h. K ∅ ∘ h = IMAGE f ∘ K ∅

⊢ K (λx. F) = K ∅

⊢ ∀B f1 f2.
    INFINITE B ∧ (∀x. f1 x ≼ B) ∧ (∀x. f2 x ≼ B) ⇒
    ∀x. S ($UNION ∘ f1) f2 x ≼ B

⊢ ∀aA bA x f g.
    (∀a. a ∈ S ($UNION ∘ aA) bA x ⇒ f a = g a) ⇒
    (∀a. a ∈ aA x ⇒ f a = g a) ∧ ∀a. a ∈ bA x ⇒ f a = g a

⊢ ∀a b x v. v ∈ a x ⇒ v ∈ S ($UNION ∘ a) b x

⊢ ∀a b x v. v ∈ b x ⇒ v ∈ S ($UNION ∘ a) b x

⊢ ∀a b x W. a x ⊆ W ∧ b x ⊆ W ⇒ S ($UNION ∘ a) b x ⊆ W

⊢ ∀aB aA bB bA mp f.
    aB ∘ mp = IMAGE f ∘ aA ∧ bB ∘ mp = IMAGE f ∘ bA ⇒
    S ($UNION ∘ aB) bB ∘ mp = IMAGE f ∘ S ($UNION ∘ aA) bA

⊢ ∀s a W. s a ⊆ W ⇒ ∀w. w ∈ {a} ⇒ s w ⊆ W

⊢ ({x} ≼ A ⇔ A ≠ ∅) ∧ ($= x ≼ A ⇔ A ≠ ∅)

⊢ S (K v) g = v ∘ g

⊢ INFINITE CC ∧ A ≼ CC ∧ B ≼ CC ⇒ A ∪ B ≼ CC

⊢ $UNION ∅ = I

⊢ (∀x. ∃!y. P x y) ⇔ ∃!f. ∀x. P x (f x)

⊢ 𝕌(:β) ≼ 𝕌(:α + β)

⊢ 𝕌(:α) ≼ 𝕌(:α + β)

⊢ 𝕌(:num) ≠ ∅

⊢ (∀a1. a1 ∈ fset fn ⇒ f1 a1 = g1 a1) ⇒ f1 ∘ fn = g1 ∘ fn

⊢ ∀f fn. fset (f ∘ fn) = IMAGE f (fset fn)

⊢ $o I = I

⊢ $o f1 ∘ $o g1 = $o (f1 ∘ g1)

⊢ ∀f. fset f ≼ 𝕌(:'b1)

⊢ ∀v. v ∈ fset (K v)

⊢ ∀a1. fset (K a1) ⊆ {a1}

⊢ (∀x. f (g x) = h x) ⇔ f ∘ g = h

⊢ (∀a1. a1 ∈ optSET x ⇒ f1 a1 = g1 a1) ⇒ OPTION_MAP f1 x = OPTION_MAP g1 x

⊢ ∀f x. optSET (OPTION_MAP f x) = IMAGE f (optSET x)

⊢ OPTION_MAP I = I

⊢ OPTION_MAP f1 ∘ OPTION_MAP g1 = OPTION_MAP (f1 ∘ g1)

⊢ ∀x. optSET x ≼ 𝕌(:num)

⊢ ∀v. v ∈ optSET (SOME v)

⊢ ∀a1. optSET (K NONE a1) ⊆ ∅

⊢ ∀a1. optSET (SOME a1) ⊆ {a1}

⊢ option_size f (OPTION_MAP g x) = option_size (λa. f (g a)) x

⊢ (∀a1. a1 ∈ setFST p ⇒ f1 a1 = g1 a1) ∧
  (∀a2. a2 ∈ setSND p ⇒ f2 a2 = g2 a2) ⇒
  (f1 ## f2) p = (g1 ## g2) p

⊢ ∀f1 f2 p. setFST ((f1 ## f2) p) = IMAGE f1 (setFST p)

⊢ ∀f1 f2 p. setSND ((f1 ## f2) p) = IMAGE f2 (setSND p)

⊢ I ## I = I

⊢ (f1 ## f2) ∘ (g1 ## g2) = f1 ∘ g1 ## f2 ∘ g2

⊢ ∀p. setFST p ≼ 𝕌(:num)

⊢ ∀p. setSND p ≼ 𝕌(:num)

⊢ ∀v. v ∈ setFST (flip $, ARB v)

⊢ ∀v. v ∈ setSND (ARB,v)

⊢ pair_size f g ((h ## k) p) = pair_size (λa. f (h a)) (λb. g (k b)) p

⊢ ∀a1 a2. setFST (a1,a2) ⊆ {a1} ∧ setSND (a1,a2) ⊆ {a2}

⊢ (∀a. a ∈ setL ab ⇒ f1 a = f2 a) ∧ (∀b. b ∈ setR ab ⇒ g1 b = g2 b) ⇒
  SUM_MAP f1 g1 ab = SUM_MAP f2 g2 ab

⊢ ∀f1 f2 s. setL (SUM_MAP f1 f2 s) = IMAGE f1 (setL s)

⊢ ∀f1 f2 s. setR (SUM_MAP f1 f2 s) = IMAGE f2 (setR s)

⊢ ∀s. setL s ≼ 𝕌(:num)

⊢ ∀s. setR s ≼ 𝕌(:num)

⊢ ∀v. v ∈ setL (INL v)

⊢ ∀v. v ∈ setR (INR v)

⊢ full_sum_size f g (SUM_MAP h k s) =
  full_sum_size (λa. f (h a)) (λb. g (k b)) s

⊢ ∀a1 a2. setL ((K ∘ INL) a1 a2) ⊆ {a1} ∧ setR ((K ∘ INL) a1 a2) ⊆ ∅

⊢ ∀a1 a2. setL (K INR a1 a2) ⊆ ∅ ∧ setR (K INR a1 a2) ⊆ {a2}