Theory: bnfMutual

Type operators

(none)

Constants

bnfMUTITER : ('fn1 -> 'n1) -> ('fn2 -> 'n2) -> (('n1 -> α) -> ('n2 -> β) -> 'fn1 -> γ) -> (('n1 -> α) -> ('n2 -> β) -> 'fn2 -> δ) -> bool
bnfMUTMAP : (('n1 -> 'c1) -> 'fn1 -> 'fg1) -> ((α -> β) -> 'fg1 -> γ) -> (('n1 -> 'c1) -> (δ -> β) -> 'fn1 -> γ) -> (('n1 -> 'c1) -> δ -> α) -> bool
bnfMUTREC : ('fn1 -> 'n1) -> ('fn2 -> 'n2) -> (('n1 -> α) -> ('n2 -> β) -> 'fn1 -> γ) -> (('n1 -> α) -> ('n2 -> β) -> 'fn2 -> δ) -> (γ -> α) -> (δ -> β) -> ('n1 -> α) -> ('n2 -> β) -> bool
bnfMUTSPLIT : (('n1 -> 'c1) -> ('n2 -> 'c2) -> 'fn2 -> 'fc2) -> (('n1 -> 'c1) -> α -> 'fc2) -> (('n2 -> 'c2) -> 'fn2 -> α) -> bool
bnfMapComp2 : (('a1 -> 'b1) -> ('a2 -> 'b2) -> ζ -> η) -> (('b1 -> 'c1) -> ('b2 -> 'c2) -> η -> θ) -> (('a1 -> 'c1) -> ('a2 -> 'c2) -> ζ -> θ) -> bool
bnfMapId2 : ((α -> α) -> (β -> β) -> ζ -> ζ) -> bool
bnfNESTSET : ('fn1 -> 'n1 -> bool) -> ('fn1 -> 'n1 -> bool) -> ('fn1 -> α -> bool) -> (α -> 'n1 -> bool) -> bool
bnfSMAP : ('fn2 -> 'n2) -> (α -> β) -> (γ -> 'fn2 -> α) -> (γ -> 'n2 -> β) -> bool
bnfSREC : (ζ -> ξ) -> ((ξ -> γ) -> ζ -> η) -> bool

Definitions

MUTITER_def MUTMAP_def MUTREC_def MUTSPLIT_def MapComp2_def MapId2_def NESTSET_def SMAP_def SREC_def

Theorems

MUTUAL_INDUCTION MUTUAL_PRIM_REC MUTUAL_RECURSION

Definitions

MUTITER_def

⊢ ∀cn1 cn2 mpK mpQ.
    bnfMUTITER cn1 cn2 mpK mpQ ⇔
    ∀t1 t2.
      (∃h1 h2. bnfMUTREC cn1 cn2 mpK mpQ t1 t2 h1 h2) ∧
      ∀h1 h2 k1 k2.
        bnfMUTREC cn1 cn2 mpK mpQ t1 t2 h1 h2 ∧
        bnfMUTREC cn1 cn2 mpK mpQ t1 t2 k1 k2 ⇒
        h1 = k1 ∧ h2 = k2

MUTMAP_def

⊢ ∀mpG mpH mpK smap.
    bnfMUTMAP mpG mpH mpK smap ⇔
    ∀g k af. mpH k (mpG g af) = mpK g (k ∘ smap g) af

MUTREC_def

⊢ ∀cn1 cn2 mpK mpQ t1 t2 h1 h2.
    bnfMUTREC cn1 cn2 mpK mpQ t1 t2 h1 h2 ⇔
    (∀af. h1 (cn1 af) = t1 (mpK h1 h2 af)) ∧
    ∀af. h2 (cn2 af) = t2 (mpQ h1 h2 af)

MUTSPLIT_def

⊢ ∀mpQ mp1a mp2n.
    bnfMUTSPLIT mpQ mp1a mp2n ⇔ ∀g k af. mpQ g k af = mp1a g (mp2n k af)

MapComp2_def

⊢ ∀mp_ab mp_bc mp_ac.
    bnfMapComp2 mp_ab mp_bc mp_ac ⇔
    ∀f1 f2 g1 g2 x.
      mp_bc g1 g2 (mp_ab f1 f2 x) = mp_ac (g1 ∘ f1) (g2 ∘ f2) x

MapId2_def

⊢ ∀mp. bnfMapId2 mp ⇔ ∀x. mp I I x = x

NESTSET_def

⊢ ∀stn1 sb1 sa1 S21.
    bnfNESTSET stn1 sb1 sa1 S21 ⇔
    ∀af. stn1 af = sb1 af ∪ BIGUNION (IMAGE S21 (sa1 af))

SMAP_def

⊢ ∀cn2 cm2 mpBg smap.
    bnfSMAP cn2 cm2 mpBg smap ⇔ ∀g af. smap g (cn2 af) = cm2 (mpBg g af)

SREC_def

⊢ ∀cn mp. bnfSREC cn mp ⇔ ∀t. ∃!h. ∀af. h (cn af) = t (mp h af)

Theorems

MUTUAL_INDUCTION

⊢ bnfFIXIND cn1 stn1 ∧ bnfFIXIND cn2 st2 ∧ bnfNESTSET stn1 sb1 sa1 S21 ∧
  bnfFIXSET cn2 st2 sb2 S21 ⇒
  ∀P1 P2.
    (∀af. (∀y. y ∈ sb1 af ⇒ P1 y) ∧ (∀z. z ∈ sa1 af ⇒ P2 z) ⇒ P1 (cn1 af)) ∧
    (∀af. (∀y. y ∈ sb2 af ⇒ P1 y) ∧ (∀z. z ∈ st2 af ⇒ P2 z) ⇒ P2 (cn2 af)) ⇒
    (∀n. P1 n) ∧ ∀m. P2 m

MUTUAL_PRIM_REC

⊢ bnfMUTITER cn1 cn2 mpq1 mpq2 ∧ bnfMUTITER cn1 cn2 mpn1 mpn2 ∧
  bnfMapComp2 mpq1 mpqn1 mpn1 ∧ bnfMapComp2 mpq1 mpqc1 mpc1 ∧
  bnfMapId2 mpn1 ∧ bnfMapComp2 mpq2 mpqn2 mpn2 ∧
  bnfMapComp2 mpq2 mpqc2 mpc2 ∧ bnfMapId2 mpn2 ⇒
  ∀t1 t2.
    (∃h1 h2.
       (∀af. h1 (cn1 af) = t1 af (mpc1 h1 h2 af)) ∧
       ∀af. h2 (cn2 af) = t2 af (mpc2 h1 h2 af)) ∧
    ∀h1 h2 k1 k2.
      ((∀af. h1 (cn1 af) = t1 af (mpc1 h1 h2 af)) ∧
       ∀af. h2 (cn2 af) = t2 af (mpc2 h1 h2 af)) ∧
      (∀af. k1 (cn1 af) = t1 af (mpc1 k1 k2 af)) ∧
      (∀af. k2 (cn2 af) = t2 af (mpc2 k1 k2 af)) ⇒
      h1 = k1 ∧ h2 = k2

MUTUAL_RECURSION

⊢ bnfSREC cn1 mpG ∧ bnfSREC cm2 mp2c ∧ bnfSREC cn2 mp2n ∧
  bnfSMAP cn2 cm2 mpBg smap ∧ bnfMUTMAP mpG mpH mpK smap ∧
  bnfMUTMAP mpBg mp2c mpQ smap ∧ bnfMUTSPLIT mpQ mp1a mp2n ⇒
  bnfMUTITER cn1 cn2 mpK mpQ

Theory bnfMutual

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems