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 ∅

⊢ $= x = {x}

⊢ 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

⊢ x ∈ $= y ⇔ x = y

⊢ K (λx. F) = K ∅

⊢ ({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)

⊢ (∀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)

⊢ (∀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)

⊢ (∀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)

⊢ (∀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)