Theory bnfFixBNF

⊢ ∀cn stn.
    bnfFIXIND cn stn ⇔
    ∀P. (∀af. (∀y. y ∈ stn af ⇒ P y) ⇒ P (cn af)) ⇒ ∀n. P n

⊢ ∀cn cm mp M. bnfFIXMAP cn cm mp M ⇔ ∀af. M (cn af) = cm (mp M af)

⊢ ∀cn stn sbn S.
    bnfFIXSET cn stn sbn S ⇔
    ∀af. S (cn af) = sbn af ∪ BIGUNION (IMAGE S (stn af))

⊢ ∀mp1 mp2 stn sbn p q.
    bnfMapCongP mp1 mp2 stn sbn p q ⇔
    ∀h1 h2 af.
      (∀y. y ∈ stn af ⇒ h1 y = h2 y) ∧ (∀b. b ∈ sbn af ⇒ p b = q b) ⇒
      mp1 h1 af = mp2 h2 af

⊢ ∀mp sbn sbm p.
    bnfNaturalP mp sbn sbm p ⇔ ∀h af. sbm (mp h af) = IMAGE p (sbn af)

⊢ BIGUNION (IMAGE h (BIGUNION (IMAGE g X))) =
  BIGUNION (IMAGE (λx. BIGUNION (IMAGE h (g x))) X)

⊢ BIGUNION (IMAGE (λx. ∅) X) = ∅

⊢ BIGUNION (IMAGE (λx. A x ∪ B x) X) =
  BIGUNION (IMAGE A X) ∪ BIGUNION (IMAGE B X)

⊢ $= a = {a}

⊢ (∀b. b ∈ $<=> a ⇒ b) ⇔ a

⊢ bnfFIXIND cn stn ⇒
  ∀P. (∀af. (∀y. y ∈ stn af ⇒ P y) ⇒ P (cn af)) ⇒ ∀n. P n

⊢ bnfMapCongP mp1 mp2 stn sbn p q ∧ bnfFIXIND cn stn ∧
  bnfFIXSET cn stn sbn Sn ∧ bnfFIXMAP cn cm mp1 M1 ∧ bnfFIXMAP cn cm mp2 M2 ⇒
  ∀n. (∀b. b ∈ Sn n ⇒ p b = q b) ⇒ M1 n = M2 n

⊢ bnfMapCong mp stn ∧ bnfMapId mp ∧ bnfFIXIND cn stn ∧ bnfFIXMAP cn cn mp M ⇒
  ∀n. M n = n

⊢ bnfMapCong mp_np stn ∧ bnfMapComp mp_nm mp_mp mp_np ∧ bnfFIXIND cn stn ∧
  bnfFIXMAP cn cm mp_nm M1 ∧ bnfFIXMAP cm cp mp_mp M2 ∧
  bnfFIXMAP cn cp mp_np M12 ⇒
  ∀n. M2 (M1 n) = M12 n

⊢ bnfFIXSET cn stn sbn Sn ∧ INFINITE B ∧ (∀af. sbn af ≼ B) ∧
  (∀af. stn af ≼ B) ∧ bnfFIXIND cn stn ⇒
  ∀n. Sn n ≼ B

⊢ bnfFIXSET cn stn sbn Sn ∧ stn w = ∅ ⇒ Sn (cn w) = sbn w

⊢ bnfFIXSET cn stn sbn Sn ⇒ ∀af b. b ∈ sbn af ⇒ b ∈ Sn (cn af)

⊢ bnfNatural mp stn stm ∧ bnfNaturalP mp sbn sbm p ∧ bnfFIXIND cn stn ∧
  bnfFIXMAP cn cm mp M ∧ bnfFIXSET cn stn sbn Sn ∧ bnfFIXSET cm stm sbm Sm ⇒
  ∀n. Sm (M n) = IMAGE p (Sn n)

⊢ (∀b. b ∈ IMAGE f s ⇒ b) ⇔ ∀y. y ∈ s ⇒ f y

⊢ (q ⇒ p) ⇒ (p ⇔ q ∨ p)

⊢ (λx. x = a) = {a}

⊢ (λx. F) = ∅