( def _fn "sets.cam" )
;---------------------

( def flat lambda
  ( l )
  ( CONC
    ( seq
      ( if
        ( or
          ( or
            ( is STR x )
            ( is INT x )
          )
          ( is SYM x )
        )
        ( makeseq x )
        ( flat x )
      )
      ( from x l )
    )
  )
)
;---------------------

( def i1 lambda
  ( x )
  ( makeseq 1 x )
)
;---------------------

( def i2 lambda
  ( x )
  ( makeseq 2 x )
)
;---------------------

( def j606o lambda
  ( y )
  ( let
    (
      ( a
        ( p1 y )
      )
      ( b
        ( p2 y )
      )
      ( k
        ( p1 b )
      )
      ( x
        ( p2 b )
      )
    )
    ( makeseq k
      ( makeseq a x )
    )
  )
)
;---------------------

( def nilit lambda
  ( x )
  ( makeseq x nil )
)
;---------------------

( def swap lambda
  ( x )
  ( makeseq
    ( p2 x )
    ( p1 x )
  )
)
;---------------------

( def PLUS lambda
  ( s )
  ( reduce
    ( makeff ) plus s
  )
)
;---------------------

( def prod lambda
  ( f g )
  ( lambda
    ( t )
    ( makeseq
      ( f
        ( p1 t )
      )
      ( g
        ( p2 t )
      )
    )
  )
)
;---------------------

( def const lambda
  ( f g )
  ( lambda
    ( x )
    ( makeseq
      ( f x )
      ( g x )
    )
  )
)
;---------------------

( def comp lambda
  ( f g )
  ( lambda
    ( x )
    ( f
      ( g x )
    )
  )
)
;---------------------

( def Kons lambda
  ( c )
  ( lambda
    ( x ) c
  )
)
;---------------------

( def id lambda
  ( x ) x
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote curry )
        ( quote
          (
            (
              ( FF AxB C )
            )
            ( FF A FF B C )
          )
        )
      )
    )
  )
)
;---------------------

( def curry lambda
  ( f )
  ( let
    (
      ( X
        ( dom f )
      )
      ( Y
        (
          ( lambda
            ( _y_ )
            ( set
              ( p1 _x_ )
              ( from _x_ _y_ )
            )
          ) X
        )
      )
    )
    ( ff1
      ( list a
        ( ff1
          ( list
            ( p2 p )
            ( ap f p )
          )
          ( from p X
            ( equal
              ( p1 p ) a
            )
          )
        )
      )
      ( from a Y )
    )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote uncurry )
        ( quote
          (
            (
              ( FF A FF B C )
            )
            ( FF AxB C )
          )
        )
      )
    )
  )
)
;---------------------

( def uncurry lambda
  ( f )
  ( PLUS
    ( set
      ( let
        (
          ( g
            ( ap f a )
          )
        )
        ( ff1
          ( list
            ( makeseq a b )
            ( ap g b )
          )
          ( from b
            ( dom g )
          )
        )
      )
      ( from a
        ( dom f )
      )
    )
  )
)
;---------------------

( def ffAset lambda
  ( s )
  ( ff1
    ( list a nil )
    ( from a s )
  )
)
;---------------------

( def join lambda
  ( f1 f2 )
  ( ff1
    ( list a
      ( makeseq
        ( ap f1 a )
        ( ap f2 a )
      )
    )
    ( from a
      ( intersection
        ( dom f1 )
        ( dom f2 )
      )
    )
  )
)
;---------------------

( def joinInv
  ( const
    ( lambda
      ( _y_ )
      ( ff1
        ( list _x_
          ( p1
            ( ap _y_ _x_ )
          )
        )
        ( from _x_
          ( dom _y_ )
        )
      )
    )
    ( lambda
      ( _y_ )
      ( ff1
        ( list _x_
          ( p2
            ( ap _y_ _x_ )
          )
        )
        ( from _x_
          ( dom _y_ )
        )
      )
    )
  )
)
;---------------------

( def uplus lambda
  ( p )
  ( plus
    ( p1 p )
    ( p2 p )
  )
)
;---------------------

( def ujoin lambda
  ( p )
  ( join
    ( p1 p )
    ( p2 p )
  )
)
;---------------------

( def nJoin
  ( comp ujoin
    ( const p1
      ( comp uplus
        ( prod
          ( lambda
            ( _y_ )
            ( ff1
              ( list _x_
                (
                  ( Kons nil )
                  ( ap _y_ _x_ )
                )
              )
              ( from _x_
                ( dom _y_ )
              )
            )
          ) curry
        )
      )
    )
  )
)
;---------------------

( def nJoinInv
  ( const
    ( lambda
      ( _y_ )
      ( ff1
        ( list _x_
          ( p1
            ( ap _y_ _x_ )
          )
        )
        ( from _x_
          ( dom _y_ )
        )
      )
    )
    ( comp uncurry
      ( lambda
        ( _y_ )
        ( ff1
          ( list _x_
            ( p2
              ( ap _y_ _x_ )
            )
          )
          ( from _x_
            ( dom _y_ )
          )
        )
      )
    )
  )
)
;---------------------

( def pJoinInv lambda
  ( f )
  ( let
    (
      ( a
        ( ff1
          ( list
            ( p2 x )
            ( ap f x )
          )
          ( from x
            ( dom f )
            ( equal
              ( p1 x ) 1
            )
          )
        )
      )
      ( b
        ( ff1
          ( list
            ( p2 x )
            ( ap f x )
          )
          ( from x
            ( dom f )
            ( equal
              ( p1 x ) 2
            )
          )
        )
      )
    )
    ( makeseq a b )
  )
)
;---------------------

( def discollect lambda
  ( f )
  ( UNION
    ( set
      ( set
        ( makeseq a b )
        ( from b
          ( ap f a )
        )
      )
      ( from a
        ( dom f )
      )
    )
  )
)
;---------------------

( def collect lambda
  ( r )
  ( ff1
    ( list a
      ( set
        ( p2 q )
        ( from q r
          ( equal a
            ( p1 q )
          )
        )
      )
    )
    ( from a
      ( set
        ( p1 p )
        ( from p r )
      )
    )
  )
)
;---------------------

( def pair2ff lambda
  ( p )
  ( makeff
    ( "Att1"
      ( p1 p )
    )
    ( "Att2"
      ( p2 p )
    )
  )
)
;---------------------
;seq2ff(t)= let (f=lambda(i)."Att"++itoa(i)) in (f->*)(seq2ff(t));

( def ff2pair lambda
  ( f )
  ( ff2seq f "" )
)
;---------------------

( def mkr lambda
  ( f )
  ( set
    ( makeseq a
      ( ap f a )
    )
    ( from a
      ( dom f )
    )
  )
)
;---------------------

( def mkf lambda
  ( r )
  ( ff1
    ( list
      ( p1 t )
      ( p2 t )
    )
    ( from t r )
  )
)
;---------------------

( def rinv lambda
  ( r )
  ( set
    ( makeseq
      ( p2 p )
      ( p1 p )
    )
    ( from p r )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote f822 )
        ( quote
          (
            (
              ( AxB )
            )
            ( BxA )
          )
        )
      )
    )
  )
)
;---------------------

( def f822 lambda
  ( p )
  ( makeseq
    ( p2 p )
    ( p1 p )
  )
)
;---------------------

( def f870 uncurry )
;---------------------

( def f87x curry )
;---------------------

( def flatten lambda
  ( r )
  ( UNION
    ( set
      ( set
        ( makeseq
          ( p1 p ) b
        )
        ( from b
          ( p2 p )
        )
      )
      ( from p r )
    )
  )
)
;---------------------

( def rcircle lambda
  ( r s )
  ( set
    ( makeseq
      ( p1 p )
      ( p2 q )
    )
    ( from p r )
    ( from q s
      ( equal
        ( p2 p )
        ( p1 q )
      )
    )
  )
)
;---------------------