;--------------------------------------------------------------------
; RSC-REPOSITORY                                               SET/97
;--------------------------------------------------------------------
;                  Copyright@1996 by F. Luis Neves
;
; Author(s):       FLN (F. Luis Neves)
; Revisions:       25.Fev.97 Rev: 13 May, 1997 (NonRec. models)
;                            Rev: 12 Jun, 1997 (Decomposition)
;                            Rev: 22 Jul, 1997
;                                 (A->B->C) => (A->1)*(B->C)
;                            Rev: 12 Dec, 1997 (Abs/Rep functions)
;                            Rev: 3 Jan, 1998 (Final revisions)
;
;--------------------------------------------------------------------
;
; Comments: SEts Tool
;
; SETS model

( deftype EKey STR )
;---------------------

( deftype EInf EQ Sets )
;---------------------

( deftype MSets FF EKey EInf )
;---------------------
; end of SETS model
; SETS sublanguage

( deftype Cst TUP
  ( A STR )
)
;---------------------

( deftype Var TUP
  ( A STR )
)
;---------------------

( deftype List TUP
  ( A Sets )
)
;---------------------

( deftype Prod TUP
  ( A LIST Sets )
)
;---------------------

( deftype Plus TUP
  ( A LIST Sets )
)
;---------------------

( deftype Pset TUP
  ( A Sets )
  ( B Sets )
)
;---------------------

( deftype Ffun TUP
  ( A Sets )
  ( B Sets )
)
;---------------------

( deftype Sets ALT Cst Var Pset List Ffun Prod Plus )
;---------------------
; end of SETS sublanguage
; SETS reificator

( deftype Reif FF RKey RInf )
;---------------------

( deftype RInf TUP
  ( Pat X )
  ( Act X )
  ( Abs STR )
  ( Rep STR )
)
;---------------------
; end of SETS reificator
;--------------------------------------------------------------------
;
; Auxiliary functions
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote fprint )
        ( quote
          (
            (
              ( STR )
              ( STR )
              ( LIST STR )
            ) NIL
          )
        )
      )
    )
  )
)
;---------------------

( def fprint lambda
  ( f m l )
  ( progn
    ( def fp
      ( fopen f m )
    )
    ( _fprint_ fp l )
    ( fclose fp )
  )
)
;---------------------

( def _fprint_ lambda
  ( f l )
  ( if
    ( equal l
      ( makeseq )
    )
    ( princ "" )
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
      )
      ( progn
        ( cond
          (
            ( is STR h )
            ( fputs h f )
          )
          (
            ( is SYM h )
            ( fputs
              ( symstr h ) f
            )
          )
          (
            ( is INT h )
            ( fputs
              ( itoa h ) f
            )
          )
          (
            ( is SYM h )
            ( fputs
              ( symstr h ) f
            )
          )
          ( true
            ( princ h )
          )
        )
        ( _fprint_ f t )
      )
    )
  )
)
;---------------------
;--------------------------------------------------------------------
;
; Subc'alculo de Isomorfismo em SETS
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR0 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR0 lambda
  ( x ) x
)
;---------------------
;
; (2.22) A x B = B x A
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR1 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR1 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "*"
        ( makeseq 'A 'B )
      )
    )
    ( O "*"
      ( makeseq
        ( RX x )
        ( LX x )
      )
    ) x
  )
)
;---------------------

( def ABS1 lambda
  ( x ) "const(p2,p1)"
)
;---------------------

( def REP1 lambda
  ( x ) "const(p2,p1)"
)
;---------------------

( def INV1 lambda
  ( x ) ""
)
;---------------------
;
; (2.23) A x (B x C) = (A x B) x C
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR2 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR2 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "*"
        ( makeseq 'A
          ( O "*"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( O "*"
      ( makeseq
        ( O "*"
          ( makeseq
            ( LX x )
            ( LX
              ( RX x )
            )
          )
        )
        ( RX
          ( RX x )
        )
      )
    ) x
  )
)
;---------------------

( def ABS2 lambda
  ( x ) "const(comp(p1,p1),const(comp(p2,p1),p2))"
)
;---------------------

( def REP2 lambda
  ( x ) "const(const(p1,comp(p1,p2)),comp(p2,p2))"
)
;---------------------

( def INV2 lambda
  ( x ) ""
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR3 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR3 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "*"
        ( makeseq
          ( O "*"
            ( makeseq 'A 'B )
          ) 'C
        )
      )
    )
    ( O "*"
      ( makeseq
        ( LX
          ( LX x )
        )
        ( O "*"
          ( makeseq
            ( RX
              ( LX x )
            )
            ( RX x )
          )
        )
      )
    ) x
  )
)
;---------------------

( def ABS3 lambda
  ( x ) "const(const(p1,comp(p1,p2)),comp(p2,p2))"
)
;---------------------

( def REP3 lambda
  ( x ) "const(comp(p1,p1),const(comp(p2,p1),p2))"
)
;---------------------

( def INV3 lambda
  ( x ) ""
)
;---------------------
;
; (2.24) A x 1 = A
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR4 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR4 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "*"
        ( makeseq 'A
          ( O "1"
            ( makeseq )
          )
        )
      )
    )
    ( LX x ) x
  )
)
;---------------------

( def ABS4 lambda
  ( x ) "nilit"
)
;---------------------

( def REP4 lambda
  ( x ) "p1"
)
;---------------------

( def INV4 lambda
  ( x ) ""
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR5 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR5 lambda
  ( x )
  ( if
    ( is V x )
    ( O "*"
      ( makeseq x
        ( O "1"
          ( makeseq )
        )
      )
    ) x
  )
)
;---------------------

( def ABS5 lambda
  ( x ) "p1"
)
;---------------------

( def REP5 lambda
  ( x ) "nilit"
)
;---------------------

( def INV5 lambda
  ( x ) ""
)
;---------------------
;
; (2.25) A + B = B + A
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR6 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR6 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "+"
        ( makeseq 'A 'B )
      )
    )
    ( O "+"
      ( makeseq
        ( RX x )
        ( LX x )
      )
    ) x
  )
)
;---------------------

( def ABS6 lambda
  ( x ) ""
)
;---------------------

( def REP6 lambda
  ( x ) ""
)
;---------------------

( def INV6 lambda
  ( x ) ""
)
;---------------------
;
; (2.26) A + (B + C) = (A + B) + C
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR7 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR7 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "+"
        ( makeseq 'A
          ( O "+"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( O "+"
      ( makeseq
        ( O "+"
          ( makeseq
            ( LX x )
            ( LX
              ( RX x )
            )
          )
        )
        ( RX
          ( RX x )
        )
      )
    ) x
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR8 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR8 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "+"
        ( makeseq
          ( O "+"
            ( makeseq 'A 'B )
          ) 'C
        )
      )
    )
    ( O "+"
      ( makeseq
        ( LX
          ( LX x )
        )
        ( O "+"
          ( makeseq
            ( RX
              ( LX x )
            )
            ( RX x )
          )
        )
      )
    ) x
  )
)
;---------------------
;
; (2.27) A + 0 = A
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR9 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR9 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "+"
        ( makeseq 'A
          ( O "0"
            ( makeseq )
          )
        )
      )
    )
    ( LX x ) x
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR10 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR10 lambda
  ( x )
  ( if
    ( is V x )
    ( O "+"
      ( makeseq x
        ( O "0"
          ( makeseq )
        )
      )
    ) x
  )
)
;---------------------
;
; (2.28) A x 0 = 0
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR11 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR11 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "*"
        ( makeseq 'A
          ( O "0"
            ( makeseq )
          )
        )
      )
    )
    ( O "0"
      ( makeseq )
    ) x
  )
)
;---------------------
;
; (2.29) A x (B + C) = (A x B) + (A x C)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR12 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR12 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "*"
        ( makeseq 'A
          ( O "+"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( O "+"
      ( makeseq
        ( O "*"
          ( makeseq
            ( LX x )
            ( LX
              ( RX x )
            )
          )
        )
        ( O "*"
          ( makeseq
            ( LX x )
            ( RX
              ( RX x )
            )
          )
        )
      )
    ) x
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR13 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR13 lambda
  ( x )
  ( if
    ( and
      ( xMatch x
        ( O "+"
          ( makeseq
            ( O "*"
              ( makeseq 'A 'B )
            )
            ( O "*"
              ( makeseq 'A 'C )
            )
          )
        )
      )
      ( equal
        ( LX
          ( LX x )
        )
        ( LX
          ( RX x )
        )
      )
    )
    ( O "*"
      ( makeseq
        ( LX
          ( LX x )
        )
        ( O "+"
          ( makeseq
            ( RX
              ( LX x )
            )
            ( RX
              ( RX x )
            )
          )
        )
      )
    ) x
  )
)
;---------------------
;
; (2.33) A ^ 0 = 1
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR14 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR14 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "^"
        ( makeseq 'A
          ( O "0"
            ( makeseq )
          )
        )
      )
    )
    ( O "1"
      ( makeseq )
    ) x
  )
)
;---------------------
;
; (2.34) A ^ (B + C) = (A ^ B) + (A ^ C)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR15 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR15 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "^"
        ( makeseq 'A
          ( O "+"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( O "+"
      ( makeseq
        ( O "^"
          ( makeseq
            ( LX x )
            ( LX
              ( RX x )
            )
          )
        )
        ( O "^"
          ( makeseq
            ( LX x )
            ( RX
              ( RX x )
            )
          )
        )
      )
    ) x
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR16 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR16 lambda
  ( x )
  ( if
    ( and
      ( xMatch x
        ( O "+"
          ( makeseq
            ( O "^"
              ( makeseq 'A 'B )
            )
            ( O "^"
              ( makeseq 'A 'C )
            )
          )
        )
      )
      ( equal
        ( LX
          ( LX x )
        )
        ( LX
          ( RX x )
        )
      )
    )
    ( O "^"
      ( makeseq
        ( LX
          ( LX x )
        )
        ( O "+"
          ( makeseq
            ( RX
              ( LX x )
            )
            ( RX
              ( RX x )
            )
          )
        )
      )
    ) x
  )
)
;---------------------
;
; (2.35) A ^ 1 = A
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR17 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR17 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "^"
        ( makeseq 'A
          ( O "1"
            ( makeseq )
          )
        )
      )
    )
    ( LX x ) x
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR18 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR18 lambda
  ( x )
  ( if
    ( is V x )
    ( O "^"
      ( makeseq x
        ( O "1"
          ( makeseq )
        )
      )
    ) x
  )
)
;---------------------
;
; (2.36) 1 ^ A = 1
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR19 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR19 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "^"
        ( makeseq
          ( O "1"
            ( makeseq )
          ) 'A
        )
      )
    )
    ( O "1"
      ( makeseq )
    ) x
  )
)
;---------------------
;
; (2.37) (B x C) ^ A = (B ^ A) x (C ^ A)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR20 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR20 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "^"
        ( makeseq
          ( O "*"
            ( makeseq 'B 'C )
          ) 'A
        )
      )
    )
    ( O "*"
      ( makeseq
        ( O "^"
          ( makeseq
            ( LX
              ( LX x )
            )
            ( RX x )
          )
        )
        ( O "^"
          ( makeseq
            ( RX
              ( LX x )
            )
            ( RX x )
          )
        )
      )
    ) x
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR21 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR21 lambda
  ( x )
  ( if
    ( and
      ( xMatch x
        ( O "*"
          ( makeseq
            ( O "^"
              ( makeseq 'B 'A )
            )
            ( O "^"
              ( makeseq 'C 'A )
            )
          )
        )
      )
      ( equal
        ( RX
          ( LX x )
        )
        ( RX
          ( RX x )
        )
      )
    )
    ( O "^"
      ( makeseq
        ( O "*"
          ( makeseq
            ( LX
              ( LX x )
            )
            ( LX
              ( RX x )
            )
          )
        )
        ( RX
          ( LX x )
        )
      )
    ) x
  )
)
;---------------------
;
; (2.38) C ^ (A x B) = (C ^ B) ^ A
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR22 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR22 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "^"
        ( makeseq 'C
          ( O "*"
            ( makeseq 'A 'B )
          )
        )
      )
    )
    ( O "^"
      ( makeseq
        ( O "^"
          ( makeseq
            ( LX x )
            ( RX
              ( RX x )
            )
          )
        )
        ( LX
          ( RX x )
        )
      )
    ) x
  )
)
;---------------------

( def ABS22 lambda
  ( x ) "uncurry"
)
;---------------------

( def REP22 lambda
  ( x ) "curry"
)
;---------------------

( def INV22 lambda
  ( x ) ""
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR23 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR23 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "^"
        ( makeseq
          ( O "^"
            ( makeseq 'C 'B )
          ) 'A
        )
      )
    )
    ( O "^"
      ( makeseq
        ( LX
          ( LX x )
        )
        ( O "*"
          ( makeseq
            ( RX x )
            ( RX
              ( LX x )
            )
          )
        )
      )
    ) x
  )
)
;---------------------

( def ABS23 lambda
  ( x ) "curry"
)
;---------------------

( def REP23 lambda
  ( x ) "uncurry"
)
;---------------------

( def INV23 lambda
  ( x ) ""
)
;---------------------
;
; (2.39) A -> B = (B + 1) ^ A
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR24 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR24 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq 'A 'B )
      )
    )
    ( O "^"
      ( makeseq
        ( O "+"
          ( makeseq
            ( RX x )
            ( O "1"
              ( makeseq )
            )
          )
        )
        ( LX x )
      )
    ) x
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR25 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR25 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "^"
        ( makeseq
          ( O "+"
            ( makeseq 'B
              ( O "1"
                ( makeseq )
              )
            )
          ) 'A
        )
      )
    )
    ( O "->"
      ( makeseq
        ( RX x )
        ( LX
          ( LX x )
        )
      )
    ) x
  )
)
;---------------------
;
; (2.40) A-list = A ^ n (n >= 0)
;
;FUNC RR40(x:X):X
;RETURN if xMatch(x,O("->",'N,'A))
;       then ... 
;
; (2.63) (B + C) -> A = (B -> A) x (C -> A)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR26 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR26 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq
          ( O "+"
            ( makeseq 'B 'C )
          ) 'A
        )
      )
    )
    ( O "*"
      ( makeseq
        ( O "->"
          ( makeseq
            ( LX
              ( LX x )
            )
            ( RX x )
          )
        )
        ( O "->"
          ( makeseq
            ( RX
              ( LX x )
            )
            ( RX x )
          )
        )
      )
    ) x
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR27 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR27 lambda
  ( x )
  ( if
    ( and
      ( xMatch x
        ( O "*"
          ( makeseq
            ( O "->"
              ( makeseq 'B 'A )
            )
            ( O "->"
              ( makeseq 'C 'A )
            )
          )
        )
      )
      ( equal
        ( RX
          ( LX x )
        )
        ( RX
          ( RX x )
        )
      )
    )
    ( O "->"
      ( makeseq
        ( O "+"
          ( makeseq
            ( LX
              ( LX x )
            )
            ( LX
              ( RX x )
            )
          )
        )
        ( RX
          ( LX x )
        )
      )
    ) x
  )
)
;---------------------
;
; (2.64) 0 -> A = 1
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR28 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR28 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq
          ( O "0"
            ( makeseq )
          ) 'A
        )
      )
    )
    ( O "1"
      ( makeseq )
    ) x
  )
)
;---------------------

( def ABS28 lambda
  ( x ) "[]"
)
;---------------------

( def REP28 lambda
  ( x ) "nil"
)
;---------------------

( def INV28 lambda
  ( x ) ""
)
;---------------------
;
; (2.64) A -> 1 = 2 ^ A
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR29 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR29 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq 'A
          ( O "1"
            ( makeseq )
          )
        )
      )
    )
    ( O "^"
      ( makeseq
        ( O "2"
          ( makeseq )
        )
        ( LX x )
      )
    ) x
  )
)
;---------------------

( def ABS29 lambda
  ( x ) "ffAset"
)
;---------------------

( def REP29 lambda
  ( x ) "dom"
)
;---------------------

( def INV29 lambda
  ( x ) ""
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR30 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR30 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "^"
        ( makeseq
          ( O "2"
            ( makeseq )
          ) 'A
        )
      )
    )
    ( O "->"
      ( makeseq
        ( RX x )
        ( O "1"
          ( makeseq )
        )
      )
    ) x
  )
)
;---------------------

( def ABS30 lambda
  ( x ) "dom"
)
;---------------------

( def REP30 lambda
  ( x ) "ffAset"
)
;---------------------

( def INV30 lambda
  ( x ) ""
)
;---------------------
;
; (2.64-2.65) 1 -> A = A + 1
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR31 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR31 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq
          ( O "1"
            ( makeseq )
          ) 'A
        )
      )
    )
    ( O "+"
      ( makeseq
        ( RX x )
        ( O "1"
          ( makeseq )
        )
      )
    ) x
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR32 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR32 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "+"
        ( makeseq 'A
          ( O "1"
            ( makeseq )
          )
        )
      )
    )
    ( O "->"
      ( makeseq
        ( O "1"
          ( makeseq )
        )
        ( LX x )
      )
    ) x
  )
)
;---------------------
;
; (2.65) A -> (B x C) => (A -> B) x (A -> C)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR33 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR33 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq 'A
          ( O "*"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( O "*"
      ( makeseq
        ( O "->"
          ( makeseq
            ( LX x )
            ( LX
              ( RX x )
            )
          )
        )
        ( O "->"
          ( makeseq
            ( LX x )
            ( RX
              ( RX x )
            )
          )
        )
      )
    ) x
  )
)
;---------------------

( def ABS33 lambda
  ( x ) "join"
)
;---------------------

( def REP33 lambda
  ( x ) "nJoinInv"
)
;---------------------

( def INV33 lambda
  ( x ) ""
)
;---------------------
;"dom(" ++ xString(LX(x)) ++ ") = dom(" ++ xString(RX(x)) ++ ")";
;
; (2.70) (A x B) -> C => A -> (B -> C)
;        Inv(x) = () notin rng(x)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR34 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR34 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq
          ( O "*"
            ( makeseq 'A 'B )
          ) 'C
        )
      )
    )
    ( O "->"
      ( makeseq
        ( LX
          ( LX x )
        )
        ( O "->"
          ( makeseq
            ( RX
              ( LX x )
            )
            ( RX x )
          )
        )
      )
    ) x
  )
)
;---------------------

( def ABS34 lambda
  ( x ) "?"
)
;---------------------

( def REP34 lambda
  ( x ) "?"
)
;---------------------

( def INV34 lambda
  ( x ) ""
)
;---------------------
;xString(RX(x)) ++ " != []";
;
; (2.71) A -> (B -> C) => 2 ^ A x ((A x B) -> C)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR35 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR35 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq 'A
          ( O "->"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( O "*"
      ( makeseq
        ( O "^"
          ( makeseq
            ( O "2"
              ( makeseq )
            )
            ( LX x )
          )
        )
        ( O "->"
          ( makeseq
            ( O "*"
              ( makeseq
                ( LX x )
                ( LX
                  ( RX x )
                )
              )
            )
            ( RX
              ( RX x )
            )
          )
        )
      )
    ) x
  )
)
;---------------------

( def ABS35 lambda
  ( x ) "..."
)
;---------------------

( def REP35 lambda
  ( x ) "..."
)
;---------------------

( def INV35 lambda
  ( x ) ""
)
;---------------------
;
; (2.72) A -> D x (B -> C) => (A -> D) x ((A x B) -> C)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR36 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR36 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq 'A
          ( O "*"
            ( makeseq 'D
              ( O "->"
                ( makeseq 'B 'C )
              )
            )
          )
        )
      )
    )
    ( O "*"
      ( makeseq
        ( O "->"
          ( makeseq
            ( LX x )
            ( LX
              ( RX x )
            )
          )
        )
        ( O "->"
          ( makeseq
            ( O "*"
              ( makeseq
                ( LX x )
                ( LX
                  ( RX
                    ( RX x )
                  )
                )
              )
            )
            ( RX
              ( RX
                ( RX x )
              )
            )
          )
        )
      )
    ) x
  )
)
;---------------------

( def ABS36 lambda
  ( x ) "nJoin"
)
;---------------------

( def REP36 lambda
  ( x ) "nJoinInv"
)
;---------------------

( def INV36 lambda
  ( x ) ""
)
;---------------------
;"proj1(dom("++xString(RX(x))++")) in dom("++xString(LX(x))++")";
;
; (2.75) A -> (B + C) => (A -> B) x (A -> C)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR37 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR37 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq 'A
          ( O "+"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( O "*"
      ( makeseq
        ( O "->"
          ( makeseq
            ( LX x )
            ( LX
              ( RX x )
            )
          )
        )
        ( O "->"
          ( makeseq
            ( LX x )
            ( RX
              ( RX x )
            )
          )
        )
      )
    ) x
  )
)
;---------------------

( def ABS37 lambda
  ( x ) "djd"
)
;---------------------

( def REP37 lambda
  ( x ) ""
)
;---------------------

( def INV37 lambda
  ( x ) ""
)
;---------------------
;"dom(" ++ xString(LX(x)) ++ ") * dom(" ++ xString(RX(x)) ++ ") = {}";
;
; (2.9) A -> B => 2 ^ (A x B)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR38 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR38 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq 'A 'B )
      )
    )
    ( O "^"
      ( makeseq
        ( O "2"
          ( makeseq )
        )
        ( O "*"
          ( makeseq
            ( LX x )
            ( RX x )
          )
        )
      )
    ) x
  )
)
;---------------------

( def ABS38 lambda
  ( x ) "mkf"
)
;---------------------

( def REP38 lambda
  ( x ) "mkr"
)
;---------------------

( def INV38 lambda
  ( x ) ""
)
;---------------------
;"forall (a,b), (a',b') in " ++ xString(x) ++ ": (a = a' => b = b')";

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RR39 )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def RR39 lambda
  ( x )
  ( if
    ( xMatch x
      ( O "->"
        ( makeseq 'A
          ( O "->"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( O "*"
      ( makeseq
        ( O "->"
          ( makeseq
            ( LX x )
            ( O "1"
              ( makeseq )
            )
          )
        )
        ( O "->"
          ( makeseq
            ( O "*"
              ( makeseq
                ( LX x )
                ( LX
                  ( RX x )
                )
              )
            )
            ( RX
              ( RX x )
            )
          )
        )
      )
    ) x
  )
)
;---------------------
;--------------------------------------------------------------------
;
; SETS Rewrite System functionality
;

( def rrInfo
  ( makeff )
)
;---------------------
; Inequacional

( def rrReif
  ( makeff
    ( 1
      ( O "*"
        ( makeseq 'A 'B )
      )
    )
    ( 2
      ( O "*"
        ( makeseq 'A
          ( O "*"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( 3
      ( O "*"
        ( makeseq
          ( O "*"
            ( makeseq 'A 'B )
          ) 'C
        )
      )
    )
    ( 4
      ( O "*"
        ( makeseq 'A
          ( O "1"
            ( makeseq )
          )
        )
      )
    )
    ( 5 'A )
    ( 6
      ( O "+"
        ( makeseq 'A 'B )
      )
    )
    ( 7
      ( O "+"
        ( makeseq 'A
          ( O "+"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( 8
      ( O "+"
        ( makeseq
          ( O "+"
            ( makeseq 'A 'B )
          ) 'C
        )
      )
    )
    ( 9
      ( O "+"
        ( makeseq 'A
          ( O "0"
            ( makeseq )
          )
        )
      )
    )
    ( 10 'A )
    ( 11
      ( O "*"
        ( makeseq 'A
          ( O "0"
            ( makeseq )
          )
        )
      )
    )
    ( 12
      ( O "*"
        ( makeseq 'A
          ( O "+"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( 13
      ( O "+"
        ( makeseq
          ( O "*"
            ( makeseq 'A 'B )
          )
          ( O "*"
            ( makeseq 'A 'C )
          )
        )
      )
    )
    ( 14
      ( O "^"
        ( makeseq 'A
          ( O "0"
            ( makeseq )
          )
        )
      )
    )
    ( 15
      ( O "^"
        ( makeseq 'A
          ( O "+"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( 16
      ( O "+"
        ( makeseq
          ( O "^"
            ( makeseq 'A 'B )
          )
          ( O "^"
            ( makeseq 'A 'C )
          )
        )
      )
    )
    ( 17
      ( O "^"
        ( makeseq 'A
          ( O "1"
            ( makeseq )
          )
        )
      )
    )
    ( 18 'A )
    ( 19
      ( O "^"
        ( makeseq
          ( O "1"
            ( makeseq )
          ) 'A
        )
      )
    )
    ( 20
      ( O "^"
        ( makeseq
          ( O "*"
            ( makeseq 'B 'C )
          ) 'A
        )
      )
    )
    ( 21
      ( O "*"
        ( makeseq
          ( O "^"
            ( makeseq 'B 'A )
          )
          ( O "^"
            ( makeseq 'C 'A )
          )
        )
      )
    )
    ( 22
      ( O "^"
        ( makeseq 'C
          ( O "*"
            ( makeseq 'A 'B )
          )
        )
      )
    )
    ( 23
      ( O "^"
        ( makeseq
          ( O "^"
            ( makeseq 'C 'B )
          ) 'A
        )
      )
    )
    ( 24
      ( O "->"
        ( makeseq 'A 'B )
      )
    )
    ( 25
      ( O "^"
        ( makeseq
          ( O "+"
            ( makeseq 'B
              ( O "1"
                ( makeseq )
              )
            )
          ) 'A
        )
      )
    )
    ( 26
      ( O "->"
        ( makeseq
          ( O "+"
            ( makeseq 'B 'C )
          ) 'A
        )
      )
    )
    ( 27
      ( O "*"
        ( makeseq
          ( O "->"
            ( makeseq 'B 'A )
          )
          ( O "->"
            ( makeseq 'C 'A )
          )
        )
      )
    )
    ( 28
      ( O "->"
        ( makeseq
          ( O "0"
            ( makeseq )
          ) 'A
        )
      )
    )
    ( 29
      ( O "->"
        ( makeseq 'A
          ( O "1"
            ( makeseq )
          )
        )
      )
    )
    ( 30
      ( O "^"
        ( makeseq
          ( O "2"
            ( makeseq )
          ) 'A
        )
      )
    )
    ( 31
      ( O "->"
        ( makeseq
          ( O "1"
            ( makeseq )
          ) 'A
        )
      )
    )
    ( 32
      ( O "+"
        ( makeseq 'A
          ( O "1"
            ( makeseq )
          )
        )
      )
    )
    ( 33
      ( O "->"
        ( makeseq 'A
          ( O "*"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( 34
      ( O "->"
        ( makeseq
          ( O "*"
            ( makeseq 'A 'B )
          ) 'C
        )
      )
    )
    ( 35
      ( O "->"
        ( makeseq 'A
          ( O "->"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( 36
      ( O "->"
        ( makeseq 'A
          ( O "*"
            ( makeseq 'D
              ( O "->"
                ( makeseq 'B 'C )
              )
            )
          )
        )
      )
    )
    ( 37
      ( O "->"
        ( makeseq 'A
          ( O "+"
            ( makeseq 'B 'C )
          )
        )
      )
    )
    ( 38
      ( O "->"
        ( makeseq 'A 'B )
      )
    )
    ( 39
      ( O "->"
        ( makeseq 'A
          ( O "->"
            ( makeseq 'B 'C )
          )
        )
      )
    )
  )
)
;---------------------
; Inequacional

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote rrINIT )
        ( quote
          (
            ( )
            ( Reif )
          )
        )
      )
    )
  )
)
;---------------------

( def rrINIT lambda
  ( )
  ( def rrInfo
    ( makeff
      ( 1
        ( RInf
          ( ap rrReif 1 )
          ( RR1
            ( ap rrReif 1 )
          ) "const(p2,p1)" "const(p2,p1)"
        )
      )
      ( 2
        ( RInf
          ( ap rrReif 2 )
          ( RR2
            ( ap rrReif 2 )
          ) "?" "?"
        )
      )
      ( 3
        ( RInf
          ( ap rrReif 3 )
          ( RR3
            ( ap rrReif 3 )
          ) "?" "?"
        )
      )
      ( 4
        ( RInf
          ( ap rrReif 4 )
          ( RR4
            ( ap rrReif 4 )
          ) "?" "?"
        )
      )
      ( 5
        ( RInf
          ( ap rrReif 5 )
          ( RR5
            ( ap rrReif 5 )
          ) "?" "?"
        )
      )
      ( 6
        ( RInf
          ( ap rrReif 6 )
          ( RR6
            ( ap rrReif 6 )
          ) "?" "?"
        )
      )
      ( 7
        ( RInf
          ( ap rrReif 7 )
          ( RR7
            ( ap rrReif 7 )
          ) "?" "?"
        )
      )
      ( 8
        ( RInf
          ( ap rrReif 8 )
          ( RR8
            ( ap rrReif 8 )
          ) "?" "?"
        )
      )
      ( 9
        ( RInf
          ( ap rrReif 9 )
          ( RR9
            ( ap rrReif 9 )
          ) "?" "?"
        )
      )
      ( 10
        ( RInf
          ( ap rrReif 10 )
          ( RR10
            ( ap rrReif 10 )
          ) "?" "?"
        )
      )
      ( 11
        ( RInf
          ( ap rrReif 11 )
          ( RR11
            ( ap rrReif 11 )
          ) "?" "?"
        )
      )
      ( 12
        ( RInf
          ( ap rrReif 12 )
          ( RR12
            ( ap rrReif 12 )
          ) "?" "?"
        )
      )
      ( 13
        ( RInf
          ( ap rrReif 13 )
          ( RR13
            ( ap rrReif 13 )
          ) "?" "?"
        )
      )
      ( 14
        ( RInf
          ( ap rrReif 14 )
          ( RR14
            ( ap rrReif 14 )
          ) "?" "?"
        )
      )
      ( 15
        ( RInf
          ( ap rrReif 15 )
          ( RR15
            ( ap rrReif 15 )
          ) "?" "?"
        )
      )
      ( 16
        ( RInf
          ( ap rrReif 16 )
          ( RR16
            ( ap rrReif 16 )
          ) "?" "?"
        )
      )
      ( 17
        ( RInf
          ( ap rrReif 17 )
          ( RR17
            ( ap rrReif 17 )
          ) "?" "?"
        )
      )
      ( 18
        ( RInf
          ( ap rrReif 18 )
          ( RR18
            ( ap rrReif 18 )
          ) "?" "?"
        )
      )
      ( 19
        ( RInf
          ( ap rrReif 19 )
          ( RR19
            ( ap rrReif 19 )
          ) "?" "?"
        )
      )
      ( 20
        ( RInf
          ( ap rrReif 20 )
          ( RR20
            ( ap rrReif 20 )
          ) "?" "?"
        )
      )
      ( 21
        ( RInf
          ( ap rrReif 21 )
          ( RR21
            ( ap rrReif 21 )
          ) "?" "?"
        )
      )
      ( 22
        ( RInf
          ( ap rrReif 22 )
          ( RR22
            ( ap rrReif 22 )
          ) "uncurry" "curry"
        )
      )
      ( 23
        ( RInf
          ( ap rrReif 23 )
          ( RR23
            ( ap rrReif 23 )
          ) "curry" "uncurry"
        )
      )
      ( 24
        ( RInf
          ( ap rrReif 24 )
          ( RR24
            ( ap rrReif 24 )
          ) "?" "?"
        )
      )
      ( 25
        ( RInf
          ( ap rrReif 25 )
          ( RR25
            ( ap rrReif 25 )
          ) "?" "?"
        )
      )
      ( 26
        ( RInf
          ( ap rrReif 26 )
          ( RR26
            ( ap rrReif 26 )
          ) "?" "?"
        )
      )
      ( 27
        ( RInf
          ( ap rrReif 27 )
          ( RR27
            ( ap rrReif 27 )
          ) "?" "?"
        )
      )
      ( 28
        ( RInf
          ( ap rrReif 28 )
          ( RR28
            ( ap rrReif 28 )
          ) "?" "?"
        )
      )
      ( 29
        ( RInf
          ( ap rrReif 29 )
          ( RR29
            ( ap rrReif 29 )
          ) "ffAset" "dom"
        )
      )
      ( 30
        ( RInf
          ( ap rrReif 30 )
          ( RR30
            ( ap rrReif 30 )
          ) "dom" "ffAset"
        )
      )
      ( 31
        ( RInf
          ( ap rrReif 31 )
          ( RR31
            ( ap rrReif 31 )
          ) "?" "?"
        )
      )
      ( 32
        ( RInf
          ( ap rrReif 32 )
          ( RR32
            ( ap rrReif 32 )
          ) "?" "?"
        )
      )
      ( 33
        ( RInf
          ( ap rrReif 33 )
          ( RR33
            ( ap rrReif 33 )
          ) "join" "nJoinInv"
        )
      )
      ( 34
        ( RInf
          ( ap rrReif 34 )
          ( RR34
            ( ap rrReif 34 )
          ) "pcurry" "puncurry"
        )
      )
      ( 35
        ( RInf
          ( ap rrReif 35 )
          ( RR35
            ( ap rrReif 35 )
          ) "nJoin" "nJoinInv"
        )
      )
      ( 36
        ( RInf
          ( ap rrReif 36 )
          ( RR36
            ( ap rrReif 36 )
          ) "nJoin" "nJoinInv"
        )
      )
      ( 37
        ( RInf
          ( ap rrReif 37 )
          ( RR37
            ( ap rrReif 37 )
          ) "coJoin" "coJoinInv"
        )
      )
      ( 38
        ( RInf
          ( ap rrReif 38 )
          ( RR38
            ( ap rrReif 38 )
          ) "mkf" "mkr"
        )
      )
      ( 39
        ( RInf
          ( ap rrReif 39 )
          ( RR39
            ( ap rrReif 39 )
          ) "nJoin" "nJoinInv"
        )
      )
    )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote rrSHOW )
        ( quote
          (
            (
              ( INT )
            ) NIL
          )
        )
      )
    )
  )
)
;---------------------

( def rrSHOW lambda
  ( i )
  ( if
    ( member i
      ( dom rrReif )
    )
    ( let
      (
        ( e
          ( ap rrReif i )
        )
      )
      ( append
        ( append
          ( xString e )
          ( makeseq "=>" )
        )
        ( xString
          ( RootMatch e i )
        )
      )
    )
    ( strcat "ERROR (precondition violated) in function " "rrSHOW" )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote ReifStep )
        ( quote
          (
            (
              ( STR )
              ( STR )
              ( STR )
            ) NIL
          )
        )
      )
    )
  )
)
;---------------------

( def ReifStep lambda
  ( a r i )
  ( princ "\nabs = " a "\nrep = " r "\ninv = " i )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote rrGetPat )
        ( quote
          (
            (
              ( INT )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def rrGetPat lambda
  ( i )
  ( if
    ( and
      ( and
        ( nequal rrInfo
          ( makeff )
        )
        ( gt i 0 )
      )
      ( lt i 40 )
    )
    ( Pat
      ( ap rrInfo i )
    )
    ( strcat "ERROR (precondition violated) in function " "rrGetPat" )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote rrGetAct )
        ( quote
          (
            (
              ( INT )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def rrGetAct lambda
  ( i )
  ( if
    ( and
      ( and
        ( nequal rrInfo
          ( makeff )
        )
        ( gt i 0 )
      )
      ( lt i 40 )
    )
    ( Act
      ( ap rrInfo i )
    )
    ( strcat "ERROR (precondition violated) in function " "rrGetAct" )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote rrGetAbs )
        ( quote
          (
            (
              ( INT )
            ) NIL
          )
        )
      )
    )
  )
)
;---------------------

( def rrGetAbs lambda
  ( i )
  ( if
    ( and
      ( and
        ( nequal rrInfo
          ( makeff )
        )
        ( gt i 0 )
      )
      ( lt i 40 )
    )
    ( Abs
      ( ap rrInfo i )
    )
    ( strcat "ERROR (precondition violated) in function " "rrGetAbs" )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote rrGetRep )
        ( quote
          (
            (
              ( INT )
            ) NIL
          )
        )
      )
    )
  )
)
;---------------------

( def rrGetRep lambda
  ( i )
  ( if
    ( and
      ( and
        ( nequal rrInfo
          ( makeff )
        )
        ( gt i 0 )
      )
      ( lt i 40 )
    )
    ( Rep
      ( ap rrInfo i )
    )
    ( strcat "ERROR (precondition violated) in function " "rrGetRep" )
  )
)
;---------------------
;          foreach(i,inseg(32),fprint("_","a",SETS2TEX(xSets(rrGetPat(i)))),
;                              fprint("_","a",SETS2TEX(xSets(rrGetAct(i)))),

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote rrSAVE )
        ( quote
          (
            ( ) NIL
          )
        )
      )
    )
  )
)
;---------------------

( def rrSAVE lambda
  ( )
  ( progn
    ( rrINIT )
    ( def fp
      ( fopen "_" "w" )
    )
    ( fprint "_" "a"
      ( makeseq "\\documentstyle{article}\n" )
    )
    ( fprint "_" "a"
      ( makeseq "\\begin{document}\n" )
    )
    ( fprint "_" "a"
      ( makeseq "\\begin{eqnarray}\n" )
    )
    ( foreach i
      ( inseg 32 )
      ( fprint "_" "a"
        ( xTeX
          ( rrGetPat i )
        )
      )
      ( fprint "_" "a"
        ( makeseq "& \\cong_{" i "} &" )
      )
      ( fprint "_" "a"
        ( xTeX
          ( rrGetAct i )
        )
      )
      ( fprint "_" "a"
        ( makeseq "\\\\\n" )
      )
    )
    ( foreach i
      ( makeseq 33 34 35 36 37 38 39 )
      ( fprint "_" "a"
        ( SETS2TEX
          ( xSets
            ( rrGetPat i )
          )
        )
      )
      ( fprint "_" "a"
        ( makeseq "& \\unlhd_{" i "} &" )
      )
      ( fprint "_" "a"
        ( SETS2TEX
          ( xSets
            ( rrGetAct i )
          )
        )
      )
      ( fprint "_" "a"
        ( makeseq "\\\\" )
      )
    )
    ( fprint "_" "a"
      ( makeseq "\n\\end{eqnarray}" )
    )
    ( fprint "_" "a"
      ( makeseq "\\end{document}\n" )
    )
    ( sh "mv _ _rules_.tex" )
  )
)
;---------------------
;
; SETS Functionality
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote CAM2SETS )
        ( quote
          (
            (
              ( STR )
            )
            ( MSets )
          )
        )
      )
    )
  )
)
;---------------------

( def CAM2SETS lambda
  ( f )
  ( progn
    ( sh
      ( strcat
        ( strcat "seca " f ) " > _1_"
      )
    )
    ( sh "./cam2set < _1_ > _2_" )
    ( nload "_2_" )
    ( sh "rm -f _1_ _2_" )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote XMT2SETS )
        ( quote
          (
            (
              ( STR )
            )
            ( MSets )
          )
        )
      )
    )
  )
)
;---------------------

( def XMT2SETS lambda
  ( f )
  ( progn
    ( sh
      ( strcat
        ( strcat "seca " f ) " > _1_"
      )
    )
    ( sh "./cam2set < _1_ > _2_" )
    ( sh "seca _2_ > _3_" )
    ( load "_3_" )
    ( sh "rm -f _1_ _2_ _3_" )
  )
)
;---------------------
;
; Flat Sets Model
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote FLATSETS )
        ( quote
          (
            (
              ( EKey )
              ( MSets )
            )
            ( Sets )
          )
        )
      )
    )
  )
)
;---------------------

( def FLATSETS lambda
  ( k s )
  ( if
    ( member k
      ( dom s )
    )
    ( makeff
      ( k
        ( _FlatSets_ k
          ( ap s k ) s
        )
      )
    )
    ( strcat "ERROR (precondition violated) in function " "FLATSETS" )
  )
)
;---------------------

( def _FlatSets_ lambda
  ( k e s )
  ( let
    (
      ( f
        ( _SetsSubst_ k e s )
      )
    )
    ( if
      ( equal e f ) e
      ( _FlatSets_ k f s )
    )
  )
)
;---------------------
;                              in if v in dom(s) then s[v] else e

( def _SetsSubst_ lambda
  ( k e s )
  ( if
    ( is Cst e ) e
    ( if
      ( is Var e )
      ( let
        (
          ( v
            ( A e )
          )
        )
        ( if
          ( and
            ( member v
              ( dom s )
            )
            ( nequal v k )
          )
          ( if
            ( is Cst
              ( ap s v )
            ) e
            ( ap s v )
          ) e
        )
      )
      ( if
        ( is Pset e )
        ( Pset
          ( _SetsSubst_ k
            ( A e ) s
          )
          ( _SetsSubst_ k
            ( B e ) s
          )
        )
        ( if
          ( is List e )
          ( List
            ( _SetsSubst_ k
              ( A e ) s
            )
          )
          ( if
            ( is Ffun e )
            ( Ffun
              ( _SetsSubst_ k
                ( A e ) s
              )
              ( _SetsSubst_ k
                ( B e ) s
              )
            )
            ( if
              ( is Prod e )
              ( Prod
                ( seq
                  ( _SetsSubst_ k x s )
                  ( from x
                    ( A e )
                  )
                )
              )
              ( if
                ( is Plus e )
                ( Plus
                  ( seq
                    ( _SetsSubst_ k x s )
                    ( from x
                      ( A e )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------
;
; Sets Decomposition
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote SETSDEC )
        ( quote
          (
            (
              ( Sets )
            )
            ( ALT FF INT Sets Sets )
          )
        )
      )
    )
  )
)
;---------------------

( def SETSDEC lambda
  ( e )
  ( if
    ( is Prod e )
    ( if
      ( member 'true
        ( set
          ( and
            ( is Cst x )
            ( is Var x )
          )
          ( from x
            ( A e )
          )
        )
      ) e
      ( ff1
        ( list i
          ( nth i
            ( A e )
          )
        )
        ( from i
          ( inseg
            ( length
              ( A e )
            )
          )
        )
      )
    ) e
  )
)
;---------------------
;
; X-Expression to Sets format
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xSets )
        ( quote
          (
            (
              ( X )
            )
            ( Sets )
          )
        )
      )
    )
  )
)
;---------------------

( def xSets lambda
  ( x )
  ( if
    ( isC x )
    ( Cst
      ( OX x )
    )
    ( if
      ( is V x )
      ( Var
        ( symstr x )
      )
      ( let
        (
          ( o
            ( OX x )
          )
          ( l
            ( LX x )
          )
          ( r
            ( RX x )
          )
        )
        ( cond
          (
            ( equal o "*" )
            ( if
              ( xProdOrio x )
              ( Prod
                ( xFlatOrio x )
              )
              ( Prod
                ( makeseq
                  ( xSets l )
                  ( xSets r )
                )
              )
            )
          )
          (
            ( equal o "+" )
            ( if
              ( xPlusOrio x )
              ( Plus
                ( xFlatOrio x )
              )
              ( Plus
                ( makeseq
                  ( xSets l )
                  ( xSets r )
                )
              )
            )
          )
          (
            ( equal o "^" )
            ( Pset
              ( xSets l )
              ( xSets r )
            )
          )
          (
            ( equal o "->" )
            ( if
              ( equal l 'N )
              ( List
                ( xSets r )
              )
              ( Ffun
                ( xSets l )
                ( xSets r )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xProdOrio )
        ( quote
          (
            (
              ( X )
            )
            ( SYM )
          )
        )
      )
    )
  )
)
;---------------------

( def xProdOrio lambda
  ( x )
  ( if
    ( is O x )
    ( let
      (
        ( o
          ( OX x )
        )
        ( l
          ( LX x )
        )
        ( r
          ( RX x )
        )
      )
      ( if
        ( and
          ( and
            ( equal o "*" )
            ( or
              ( or
                ( is V l )
                ( isC l )
              )
              ( xProdOrio l )
            )
          )
          ( or
            ( or
              ( is V r )
              ( isC r )
            )
            ( xProdOrio r )
          )
        ) true false
      )
    ) false
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xPlusOrio )
        ( quote
          (
            (
              ( X )
            )
            ( SYM )
          )
        )
      )
    )
  )
)
;---------------------

( def xPlusOrio lambda
  ( x )
  ( if
    ( is O x )
    ( let
      (
        ( o
          ( OX x )
        )
        ( l
          ( LX x )
        )
        ( r
          ( RX x )
        )
      )
      ( if
        ( and
          ( and
            ( equal o "+" )
            ( or
              ( or
                ( is V l )
                ( isC l )
              )
              ( xPlusOrio l )
            )
          )
          ( or
            ( or
              ( is V r )
              ( isC r )
            )
            ( xPlusOrio r )
          )
        ) true false
      )
    ) false
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xFlatOrio )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def xFlatOrio lambda
  ( x )
  ( if
    ( isC x )
    ( makeseq
      ( Cst
        ( OX x )
      )
    )
    ( if
      ( is V x )
      ( makeseq
        ( Var
          ( symstr x )
        )
      )
      ( let
        (
          ( o
            ( OX x )
          )
          ( l
            ( LX x )
          )
          ( r
            ( RX x )
          )
        )
        ( append
          ( xFlatOrio l )
          ( xFlatOrio r )
        )
      )
    )
  )
)
;---------------------
;
; Abstraction function string
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xAbs2Str )
        ( quote
          (
            (
              ( X )
            )
            ( LIST STR )
          )
        )
      )
    )
  )
)
;---------------------

( def xAbs2Str lambda
  ( x )
  ( if
    ( or
      ( or
        ( isC x )
        ( is V x )
      )
      ( is F x )
    )
    ( makeseq x )
    ( let
      (
        ( o
          ( OX x )
        )
        ( l
          ( LX x )
        )
        ( r
          ( RX x )
        )
      )
      ( if
        ( and
          ( equal l "id" )
          ( equal r "id" )
        )
        ( makeseq "id" )
        ( if
          ( equal o "->" )
          ( cond
            (
              ( equal r "id" )
              ( append
                ( append
                  ( makeseq "(" )
                  ( xAbs2Str l )
                )
                ( makeseq "->*)" )
              )
            )
            (
              ( equal l "id" )
              ( append
                ( append
                  ( makeseq "(*->" )
                  ( xAbs2Str r )
                )
                ( makeseq ")" )
              )
            )
            ( true
              ( append
                ( append
                  ( xAbs2Str l )
                  ( makeseq "->" )
                )
                ( xAbs2Str r )
              )
            )
          )
          ( if
            ( equal o "*" )
            ( cond
              (
                ( equal r "id" )
                ( append
                  ( append
                    ( makeseq "prod(" )
                    ( xAbs2Str l )
                  )
                  ( makeseq ",id)" )
                )
              )
              (
                ( equal l "id" )
                ( append
                  ( append
                    ( makeseq "prod(id," )
                    ( xAbs2Str r )
                  )
                  ( makeseq ")" )
                )
              )
              ( true
                ( append
                  ( append
                    ( xAbs2Str l )
                    ( makeseq "*" )
                  )
                  ( xAbs2Str r )
                )
              )
            )
            ( if
              ( equal o "+" )
              ( cond
                (
                  ( equal r "id" )
                  ( append
                    ( append
                      ( makeseq "const(" )
                      ( xAbs2Str l )
                    )
                    ( makeseq ",id)" )
                  )
                )
                (
                  ( equal l "id" )
                  ( append
                    ( append
                      ( makeseq "const(id," )
                      ( xAbs2Str r )
                    )
                    ( makeseq ")" )
                  )
                )
                ( true
                  ( append
                    ( append
                      ( xAbs2Str l )
                      ( makeseq "*" )
                    )
                    ( xAbs2Str r )
                  )
                )
              )
              ( append
                ( append
                  ( xAbs2Str l )
                  ( makeseq o )
                )
                ( xAbs2Str r )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------
;
; Abstraction function TeX string
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xAbs2TeX )
        ( quote
          (
            (
              ( X )
            )
            ( LIST STR )
          )
        )
      )
    )
  )
)
;---------------------

( def xAbs2TeX lambda
  ( x )
  ( if
    ( or
      ( or
        ( isC x )
        ( is V x )
      )
      ( is F x )
    )
    ( makeseq x )
    ( let
      (
        ( o
          ( OX x )
        )
        ( l
          ( LX x )
        )
        ( r
          ( RX x )
        )
      )
      ( if
        ( and
          ( equal l "id" )
          ( equal r "id" )
        )
        ( makeseq "id" )
        ( if
          ( equal o "->" )
          ( cond
            (
              ( equal r "id" )
              ( append
                ( append
                  ( makeseq "(" )
                  ( xAbs2TeX l )
                )
                ( makeseq " \\hookrightarrow\\star)" )
              )
            )
            (
              ( equal l "id" )
              ( append
                ( append
                  ( makeseq "(\\star\\hookrightarrow " )
                  ( xAbs2TeX r )
                )
                ( makeseq ")" )
              )
            )
            ( true
              ( append
                ( append
                  ( xAbs2TeX l )
                  ( makeseq " \\hookrightarrow " )
                )
                ( xAbs2TeX r )
              )
            )
          )
          ( if
            ( equal o "*" )
            ( cond
              (
                ( equal r "id" )
                ( append
                  ( append
                    ( makeseq "prod(" )
                    ( xAbs2TeX l )
                  )
                  ( makeseq ",id)" )
                )
              )
              (
                ( equal l "id" )
                ( append
                  ( append
                    ( makeseq "prod(id," )
                    ( xAbs2TeX r )
                  )
                  ( makeseq ")" )
                )
              )
              ( true
                ( append
                  ( append
                    ( xAbs2TeX l )
                    ( makeseq " \\times " )
                  )
                  ( xAbs2TeX r )
                )
              )
            )
            ( if
              ( equal o "+" )
              ( cond
                (
                  ( equal r "id" )
                  ( append
                    ( append
                      ( makeseq "const(" )
                      ( xAbs2TeX l )
                    )
                    ( makeseq ",id)" )
                  )
                )
                (
                  ( equal l "id" )
                  ( append
                    ( append
                      ( makeseq "const(id," )
                      ( xAbs2TeX r )
                    )
                    ( makeseq ")" )
                  )
                )
                ( true
                  ( append
                    ( append
                      ( xAbs2TeX l )
                      ( makeseq " + " )
                    )
                    ( xAbs2TeX r )
                  )
                )
              )
              ( append
                ( append
                  ( xAbs2TeX l )
                  ( makeseq o )
                )
                ( xAbs2TeX r )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------
;
; Expression abstraction function
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xAbsFun )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def xAbsFun lambda
  ( x )
  ( cond
    (
      ( isC x ) "id"
    )
    (
      ( is V x ) "id"
    )
    (
      ( is F x ) x
    )
    ( true
      ( let
        (
          ( o
            ( OX x )
          )
          ( l
            ( LX x )
          )
          ( r
            ( RX x )
          )
        )
        ( cond
          (
            ( and
              ( equal l "id" )
              ( equal r "id" )
            ) "id"
          )
          (
            ( and
              ( equal
                ( xAbsFun l ) "id"
              )
              ( equal
                ( xAbsFun r ) "id"
              )
            ) "id"
          )
          (
            ( or
              ( equal l "id" )
              ( equal
                ( xAbsFun l ) "id"
              )
            )
            ( O o
              ( makeseq "id"
                ( xAbsFun r )
              )
            )
          )
          (
            ( or
              ( equal r "id" )
              ( equal
                ( xAbsFun r ) "id"
              )
            )
            ( O o
              ( makeseq
                ( xAbsFun l ) "id"
              )
            )
          )
          ( true
            ( O o
              ( makeseq
                ( xAbsFun l )
                ( xAbsFun r )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------
;
; Expression representation function
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xRepFun )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def xRepFun lambda
  ( x )
  ( cond
    (
      ( isC x ) "id"
    )
    (
      ( is V x ) "id"
    )
    (
      ( is F x ) x
    )
    ( true
      ( let
        (
          ( o
            ( OX x )
          )
          ( l
            ( LX x )
          )
          ( r
            ( RX x )
          )
        )
        ( O o
          ( makeseq
            ( xAbsFun l )
            ( xAbsFun r )
          )
        )
      )
    )
  )
)
;---------------------
;
; If xFirstMatch replaces the expression match with abstraction function
; x2 is the template
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xAbsMatch )
        ( quote
          (
            (
              ( STR ) ANY
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def xAbsMatch lambda
  ( a x1 x2 )
  ( if
    ( xMatch x1 x2 ) a
    ( if
      ( and
        ( is O x1 )
        ( not
          ( isC x1 )
        )
      )
      ( cond
        (
          ( equal
            ( xAbsMatch a
              ( LX x1 ) x2
            ) a
          )
          ( O
            ( OX x1 )
            ( makeseq a
              ( RX x1 )
            )
          )
        )
        (
          ( equal
            ( xAbsMatch a
              ( RX x1 ) x2
            ) a
          )
          ( O
            ( OX x1 )
            ( makeseq
              ( LX x1 ) a
            )
          )
        )
        ( true
          ( O
            ( OX x1 )
            ( makeseq
              ( xAbsMatch a
                ( LX x1 ) x2
              )
              ( xAbsMatch a
                ( RX x1 ) x2
              )
            )
          )
        )
      ) x1
    )
  )
)
;---------------------
;
; If xFirstMatch replaces the expression match with representation function
; x2 is the template
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xRepMatch )
        ( quote
          (
            (
              ( STR ) ANY
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def xRepMatch lambda
  ( r x1 x2 )
  ( if
    ( xMatch x1 x2 ) r
    ( if
      ( and
        ( is O x1 )
        ( not
          ( isC x1 )
        )
      )
      ( cond
        (
          ( equal
            ( xRepMatch r
              ( LX x1 ) x2
            ) r
          )
          ( O
            ( OX x1 )
            ( makeseq r
              ( RX x1 )
            )
          )
        )
        (
          ( equal
            ( xRepMatch r
              ( RX x1 ) x2
            ) r
          )
          ( O
            ( OX x1 )
            ( makeseq
              ( LX x1 ) r
            )
          )
        )
        ( true
          ( O
            ( OX x1 )
            ( makeseq
              ( xRepMatch r
                ( LX x1 ) x2
              )
              ( xRepMatch r
                ( RX x1 ) x2
              )
            )
          )
        )
      ) x1
    )
  )
)
;---------------------
;
; Sets to X-Expression format
;
;RETURN if is-Cst(e) then strsym(A(e))
;List(SetsSubst(A(e),s))
;(< SetsSubst(x,s) | x <- A(e) >)
;Plus(< SetsSubst(x,s) | x <- A(e) >)

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote SETS2BSETS )
        ( quote
          (
            (
              ( Sets )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def SETS2BSETS lambda
  ( e )
  ( if
    ( is Cst e )
    ( O
      ( A e )
      ( makeseq )
    )
    ( if
      ( is Var e )
      ( strsym
        ( A e )
      )
      ( if
        ( is Pset e )
        ( O "^"
          ( makeseq
            ( SETS2BSETS
              ( A e )
            )
            ( SETS2BSETS
              ( B e )
            )
          )
        )
        ( if
          ( is List e )
          ( O "->"
            ( makeseq 'N
              ( SETS2BSETS
                ( A e )
              )
            )
          )
          ( if
            ( is Ffun e )
            ( O "->"
              ( makeseq
                ( SETS2BSETS
                  ( A e )
                )
                ( SETS2BSETS
                  ( B e )
                )
              )
            )
            ( if
              ( is Prod e )
              ( ProdBinary
                ( A e )
              )
              ( if
                ( is Plus e )
                ( PlusBinary
                  ( A e )
                ) e
              )
            )
          )
        )
      )
    )
  )
)
;---------------------

( def ProdBinary lambda
  ( l )
  ( if
    ( equal l
      ( makeseq )
    ) 'error
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
      )
      ( if
        ( equal
          ( length l ) 1
        )
        ( SETS2BSETS h )
        ( if
          ( equal
            ( length l ) 2
          )
          ( O "*"
            ( makeseq
              ( SETS2BSETS h )
              ( SETS2BSETS
                ( nth 2 l )
              )
            )
          )
          ( O "*"
            ( makeseq
              ( SETS2BSETS h )
              ( ProdBinary t )
            )
          )
        )
      )
    )
  )
)
;---------------------

( def PlusBinary lambda
  ( l )
  ( if
    ( equal l
      ( makeseq )
    ) 'error
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
      )
      ( if
        ( equal
          ( length l ) 1
        )
        ( SETS2BSETS h )
        ( if
          ( equal
            ( length l ) 2
          )
          ( O "+"
            ( makeseq
              ( SETS2BSETS h )
              ( SETS2BSETS
                ( nth 2 l )
              )
            )
          )
          ( O "+"
            ( makeseq
              ( SETS2BSETS h )
              ( PlusBinary t )
            )
          )
        )
      )
    )
  )
)
;---------------------
;
; Sets to Camila
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote SETS2CAM )
        ( quote
          (
            (
              ( Sets )
            )
            ( STR )
          )
        )
      )
    )
  )
)
;---------------------

( def SETS2CAM lambda
  ( e )
  ( if
    ( is Cst e )
    ( makeseq
      ( A e )
    )
    ( if
      ( is Var e )
      ( makeseq
        ( A e )
      )
      ( if
        ( is Pset e )
        ( if
          ( equal
            ( A e ) 2
          )
          ( append
            ( append
              ( makeseq ";\n" )
              ( _Sets2CAM_
                ( A e )
              )
            )
            ( makeseq "-set" )
          )
          ( append
            ( append
              ( append
                ( append
                  ( makeseq "(" )
                  ( _Sets2CAM_
                    ( A e )
                  )
                )
                ( makeseq "^" )
              )
              ( SETS2CAM
                ( B e )
              )
            )
            ( makeseq ")" )
          )
        )
        ( if
          ( is List e )
          ( append
            ( append
              ( makeseq ";\n" )
              ( _Sets2CAM_
                ( A e )
              )
            )
            ( makeseq "-list" )
          )
          ( if
            ( is Ffun e )
            ( append
              ( append
                ( append
                  ( append
                    ( makeseq "(" )
                    ( _Sets2CAM_
                      ( A e )
                    )
                  )
                  ( makeseq "->" )
                )
                ( SETS2CAM
                  ( B e )
                )
              )
              ( makeseq ")" )
            )
            ( if
              ( is Prod e )
              ( append
                ( makeseq ";\n" )
                ( _Prod2CAM_
                  ( A e ) 1
                )
              )
              ( if
                ( is Plus e )
                ( append
                  ( makeseq ";\n" )
                  ( _Plus2CAM_
                    ( A e )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------
;                else <"("> ^ SETS2CAM(e) ^ <")">;

( def _Sets2CAM_ lambda
  ( e )
  ( if
    ( is Cst e )
    ( makeseq
      ( A e )
    )
    ( if
      ( is Var e )
      ( makeseq
        ( A e )
      )
      ( SETS2CAM e )
    )
  )
)
;---------------------
;                              <"P"++itoa(i.+1) ++ ":"> ^

( def _Prod2CAM_ lambda
  ( l i )
  ( if
    ( equal l
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
      )
      ( if
        ( equal
          ( length l ) 1
        )
        ( append
          ( makeseq
            ( strcat
              ( strcat "P"
                ( itoa i )
              ) ":"
            )
          )
          ( SETS2CAM h )
        )
        ( append
          ( append
            ( makeseq
              ( strcat
                ( strcat "P"
                  ( itoa i )
                ) ":"
              )
            )
            ( SETS2CAM h )
          )
          ( _Prod2CAM_ t
            ( add i 1 )
          )
        )
      )
    )
  )
)
;---------------------

( def _Plus2CAM_ lambda
  ( l )
  ( if
    ( equal l
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
      )
      ( if
        ( equal
          ( length l ) 1
        )
        ( SETS2CAM h )
        ( append
          ( append
            ( SETS2CAM h )
            ( makeseq "|" )
          )
          ( _Plus2CAM_ t )
        )
      )
    )
  )
)
;---------------------
;
; Sets to TeX
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote SETS2TEX )
        ( quote
          (
            (
              ( Sets )
            )
            ( STR )
          )
        )
      )
    )
  )
)
;---------------------

( def SETS2TEX lambda
  ( e )
  ( if
    ( is Cst e )
    ( makeseq
      ( A e )
    )
    ( if
      ( is Var e )
      ( makeseq
        ( A e )
      )
      ( if
        ( is Pset e )
        ( if
          ( and
            ( is Cst
              ( A e )
            )
            ( equal
              ( A
                ( A e )
              ) "2"
            )
          )
          ( append
            ( append
              ( makeseq "2^{" )
              ( _Sets2TEX_
                ( B e )
              )
            )
            ( makeseq "}" )
          )
          ( append
            ( append
              ( append
                ( append
                  ( makeseq "{" )
                  ( _Sets2TEX_
                    ( A e )
                  )
                )
                ( makeseq "}^{" )
              )
              ( SETS2TEX
                ( B e )
              )
            )
            ( makeseq "}" )
          )
        )
        ( if
          ( is List e )
          ( append
            ( append
              ( makeseq "(" )
              ( _Sets2TEX_
                ( A e )
              )
            )
            ( makeseq ")\^{\\star}" )
          )
          ( if
            ( is Ffun e )
            ( append
              ( append
                ( append
                  ( append
                    ( makeseq "(" )
                    ( _Sets2TEX_
                      ( A e )
                    )
                  )
                  ( makeseq " \\hookrightarrow " )
                )
                ( SETS2TEX
                  ( B e )
                )
              )
              ( makeseq ")" )
            )
            ( if
              ( is Prod e )
              ( _Prod2TEX_
                ( A e )
              )
              ( if
                ( is Plus e )
                ( _Plus2TEX_
                  ( A e )
                )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------
;                else <"("> ^ SETS2TEX(e) ^ <")">;

( def _Sets2TEX_ lambda
  ( e )
  ( if
    ( is Cst e )
    ( makeseq
      ( A e )
    )
    ( if
      ( is Var e )
      ( makeseq
        ( A e )
      )
      ( SETS2TEX e )
    )
  )
)
;---------------------

( def _Prod2TEX_ lambda
  ( l )
  ( if
    ( equal l
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
      )
      ( cond
        (
          ( equal
            ( length l ) 1
          )
          ( SETS2TEX h )
        )
        (
          ( equal
            ( length l ) 2
          )
          ( append
            ( append
              ( append
                ( append
                  ( makeseq "(" )
                  ( SETS2TEX h )
                )
                ( makeseq " \\times " )
              )
              ( _Prod2TEX_ t )
            )
            ( makeseq ")" )
          )
        )
        ( true
          ( append
            ( append
              ( SETS2TEX h )
              ( makeseq " \\times " )
            )
            ( _Prod2TEX_ t )
          )
        )
      )
    )
  )
)
;---------------------

( def _Plus2TEX_ lambda
  ( l )
  ( if
    ( equal l
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
      )
      ( cond
        (
          ( equal
            ( length l ) 1
          )
          ( SETS2TEX h )
        )
        (
          ( equal
            ( length l ) 2
          )
          ( append
            ( append
              ( append
                ( append
                  ( makeseq "(" )
                  ( SETS2TEX h )
                )
                ( makeseq " \\times " )
              )
              ( _Plus2TEX_ t )
            )
            ( makeseq ")" )
          )
        )
        ( true
          ( append
            ( append
              ( SETS2TEX h )
              ( makeseq " + " )
            )
            ( _Plus2TEX_ t )
          )
        )
      )
    )
  )
)
;---------------------
;
; Sets to String
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote SETS2STR )
        ( quote
          (
            (
              ( Sets )
            )
            ( STR )
          )
        )
      )
    )
  )
)
;---------------------

( def SETS2STR lambda
  ( e )
  ( if
    ( is Cst e )
    ( makeseq
      ( A e )
    )
    ( if
      ( is Var e )
      ( makeseq
        ( A e )
      )
      ( if
        ( is Pset e )
        ( if
          ( equal
            ( A e ) 2
          )
          ( append
            ( append
              ( makeseq "(" )
              ( _Sets2STR_
                ( A e )
              )
            )
            ( makeseq ")-set" )
          )
          ( append
            ( append
              ( append
                ( append
                  ( makeseq "(" )
                  ( _Sets2STR_
                    ( A e )
                  )
                )
                ( makeseq "->" )
              )
              ( SETS2STR
                ( B e )
              )
            )
            ( makeseq ")" )
          )
        )
        ( if
          ( is List e )
          ( append
            ( append
              ( makeseq "(" )
              ( _Sets2STR_
                ( A e )
              )
            )
            ( makeseq ")-list" )
          )
          ( if
            ( is Ffun e )
            ( append
              ( append
                ( append
                  ( append
                    ( makeseq "(" )
                    ( _Sets2STR_
                      ( A e )
                    )
                  )
                  ( makeseq "->" )
                )
                ( SETS2STR
                  ( B e )
                )
              )
              ( makeseq ")" )
            )
            ( if
              ( is Prod e )
              ( _Prod2STR_
                ( A e )
              )
              ( if
                ( is Plus e )
                ( _Plus2STR_
                  ( A e )
                )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------
;                else <"("> ^ SETS2STR(e) ^ <")">;

( def _Sets2STR_ lambda
  ( e )
  ( if
    ( is Cst e )
    ( makeseq
      ( A e )
    )
    ( if
      ( is Var e )
      ( makeseq
        ( A e )
      )
      ( SETS2STR e )
    )
  )
)
;---------------------

( def _Prod2STR_ lambda
  ( l )
  ( if
    ( equal l
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
      )
      ( if
        ( equal
          ( length l ) 1
        )
        ( SETS2STR h )
        ( append
          ( append
            ( SETS2STR h )
            ( makeseq " * " )
          )
          ( _Prod2STR_ t )
        )
      )
    )
  )
)
;---------------------

( def _Plus2STR_ lambda
  ( l )
  ( if
    ( equal l
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
      )
      ( if
        ( equal
          ( length l ) 1
        )
        ( SETS2STR h )
        ( append
          ( append
            ( SETS2STR h )
            ( makeseq " + " )
          )
          ( _Plus2STR_ t )
        )
      )
    )
  )
)
;---------------------
;
; Sets to File
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote SETS2FILE )
        ( quote
          (
            (
              ( Sets )
              ( STR )
            ) NIL
          )
        )
      )
    )
  )
)
;---------------------

( def SETS2FILE lambda
  ( e f )
  ( fprint f "w"
    ( SETS2STR e )
  )
)
;---------------------
;
; Non Recursive Sets Model
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote SETSNREC )
        ( quote
          (
            (
              ( EKey )
              ( MSets )
            )
            ( MSets )
          )
        )
      )
    )
  )
)
;---------------------

( def SETSNREC lambda
  ( k m )
  ( if
    ( and
      ( member k
        ( dom m )
      )
      ( SETSRENT k m )
    )
    ( plus m
      ( makeff
        ( k
          ( Prod
            ( makeseq
              ( Var "K" )
              ( Ffun
                ( Var "K" )
                ( _SetsNRec_
                  ( ap m k )
                  ( makeff
                    ( k
                      ( Var "K" )
                    )
                  )
                )
              )
            )
          )
        )
      )
    ) "Non recursive model?"
  )
)
;---------------------
;                              in if v in dom(s) then s[v] else e

( def _SetsNRec_ lambda
  ( e s )
  ( if
    ( is Cst e ) e
    ( if
      ( is Var e )
      ( let
        (
          ( v
            ( A e )
          )
        )
        ( if
          ( member v
            ( dom s )
          )
          ( if
            ( is Cst
              ( ap s v )
            ) e
            ( ap s v )
          ) e
        )
      )
      ( if
        ( is Pset e )
        ( Pset
          ( _SetsNRec_
            ( A e ) s
          )
          ( _SetsNRec_
            ( B e ) s
          )
        )
        ( if
          ( is List e )
          ( List
            ( _SetsNRec_
              ( A e ) s
            )
          )
          ( if
            ( is Ffun e )
            ( Ffun
              ( _SetsNRec_
                ( A e ) s
              )
              ( _SetsNRec_
                ( B e ) s
              )
            )
            ( if
              ( is Prod e )
              ( Prod
                ( seq
                  ( _SetsNRec_ x s )
                  ( from x
                    ( A e )
                  )
                )
              )
              ( if
                ( is Plus e )
                ( Plus
                  ( seq
                    ( _SetsNRec_ x s )
                    ( from x
                      ( A e )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------
;RETURN let (x = { m[x] | x <- SETSRENT(m,s) } U SETSRENT(m,s), y = m / x)
;in m + _SetsNRec_(y);
;_SetsNRec_(m) = let (d = [ x -> _SetsRDep_(m[x],m) | x <- dom(m) ])
;in _UnRecLaw1_(d,m);
;
; 1st UnRecursive Law
;

( def _UnRecLaw1_ lambda
  ( d s )
  ( if
    ( equal d
      ( makeff )
    )
    ( makeff )
    ( let
      (
        ( x
          ( choice
            ( dom d )
          )
        )
        ( y
          ( ap d x )
        )
      )
      ( if
        ( not
          ( member x y )
        )
        ( plus
          ( makeff
            ( x
              ( ap s x )
            )
          )
          ( _UnRecLaw1_
            ( ds d
              ( makeset x )
            ) s
          )
        )
        ( let
          (
            ( f
              ( _FlatSets_
                ( ap s x )
                ( ds s
                  ( makeset x )
                )
              )
            )
          )
          ( plus
            ( makeff
              ( x
                ( Prod
                  ( makeseq
                    ( Var "K" )
                    ( Ffun
                      ( Var "K" )
                      ( _SetsSubst_ f
                        ( makeff
                          ( x
                            ( Var "K" )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
            ( _UnRecLaw1_
              ( ds d
                ( makeset x )
              ) s
            )
          )
        )
      )
    )
  )
)
;---------------------
;
; Sets Entities Dependencies
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote SETSEDEP )
        ( quote
          (
            (
              ( EKey )
              ( MSets )
            )
            ( FF EKey SET EKey )
          )
        )
      )
    )
  )
)
;---------------------

( def SETSEDEP lambda
  ( k m )
  ( makeff
    ( k
      ( _SetsRDep_ k
        ( ap m k ) m
      )
    )
  )
)
;---------------------
;
; Sets Recursive Entities
;
;RETURN { x | x <- s : x in _SetsRDep_(k,m[k],m) };

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote SETSRENT )
        ( quote
          (
            (
              ( EKey )
              ( MSets )
            )
            ( SYM )
          )
        )
      )
    )
  )
)
;---------------------

( def SETSRENT lambda
  ( k m )
  ( if
    ( member k
      ( dom m )
    )
    ( member k
      ( _SetsRDep_ k
        ( ap m k ) m
      )
    )
    ( strcat "ERROR (precondition violated) in function " "SETSRENT" )
  )
)
;---------------------
;
; Sets Recursive Dependencies
;

( def _SetsRDep_ lambda
  ( k e m )
  ( if
    ( is Cst e )
    ( makeset )
    ( if
      ( is Var e )
      ( let
        (
          ( v
            ( A e )
          )
        )
        ( if
          ( and
            ( member v
              ( dom m )
            )
            ( nequal v k )
          )
          ( union
            ( makeset v )
            ( _SetsRDep_ k
              ( ap m v )
              ( ds m
                ( makeset v )
              )
            )
          )
          ( makeset v )
        )
      )
      ( if
        ( is Pset e )
        ( union
          ( _SetsRDep_ k
            ( A e ) m
          )
          ( _SetsRDep_ k
            ( B e ) m
          )
        )
        ( if
          ( is List e )
          ( _SetsRDep_ k
            ( A e ) m
          )
          ( if
            ( is Ffun e )
            ( union
              ( _SetsRDep_ k
                ( A e ) m
              )
              ( _SetsRDep_ k
                ( B e ) m
              )
            )
            ( if
              ( is Prod e )
              ( UNION
                ( set
                  ( _SetsRDep_ k x m )
                  ( from x
                    ( A e )
                  )
                )
              )
              ( if
                ( is Plus e )
                ( UNION
                  ( set
                    ( _SetsRDep_ k x m )
                    ( from x
                      ( A e )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)
;---------------------
;--------------------------------------------------------------------
;
; Model-Oriented Match Functionality
; 
;--------------------------------------------------------------------
;
; Degree of match
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote rscDegreeMatch )
        ( quote
          (
            (
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def rscDegreeMatch lambda
  ( x )
  ( if
    ( or
      ( erMatch x )
      ( ffMatch x )
    ) 100
    ( let
      (
        ( t
          ( sub
            ( xComplex x )
            ( xOpr x )
          )
        )
        ( m
          ( xMetaSym x )
        )
      )
      ( pdiv m t )
    )
  )
)
;---------------------
;--------------------------------------------------------------------
; ER model (Entity-Relationship)
;
;         not(xFirstMatch(RX(x),pattern)) &&

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote erMatch )
        ( quote
          (
            (
              ( X )
            )
            ( SYM )
          )
        )
      )
    )
  )
)
;---------------------

( def erMatch lambda
  ( x )
  ( let
    (
      ( pattern
        ( O "^"
          ( makeseq
            ( O "2"
              ( makeseq )
            ) 'X
          )
        )
      )
    )
    ( and
      ( xMatch x pattern )
      ( or
        ( or
          ( is V
            ( RX x )
          )
          ( isC x )
        )
        ( xProdOrio
          ( RX x )
        )
      )
    )
  )
)
;---------------------
;
; If erFirstMatch replaces the expression match with '_er_
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote erMetaMatch )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def erMetaMatch lambda
  ( x1 )
  ( if
    ( erMatch x1 ) '_er_
    ( if
      ( and
        ( is O x1 )
        ( equal
          ( OX x1 ) "*"
        )
      )
      ( cond
        (
          ( equal
            ( LX x1 ) '_er_
          )
          ( O
            ( OX x1 )
            ( makeseq '_er_
              ( erMetaMatch
                ( RX x1 )
              )
            )
          )
        )
        (
          ( equal
            ( RX x1 ) '_er_
          )
          ( O
            ( OX x1 )
            ( makeseq
              ( erMetaMatch
                ( LX x1 )
              ) '_er_
            )
          )
        )
        ( true
          ( O
            ( OX x1 )
            ( makeseq
              ( erMetaMatch
                ( LX x1 )
              )
              ( erMetaMatch
                ( RX x1 )
              )
            )
          )
        )
      ) x1
    )
  )
)
;---------------------
;
; Applies erMetaMatch until no more applications are possible
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote erApplyMetaMatch )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def erApplyMetaMatch lambda
  ( x )
  ( let
    (
      ( y
        ( erMetaMatch x )
      )
    )
    ( if
      ( equal x y ) x
      ( erApplyMetaMatch y )
    )
  )
)
;---------------------
;
; Applies A->B => 2^(A*B) until no more applications are possible
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote erApplyFinalRule )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def erApplyFinalRule lambda
  ( x )
  ( let
    (
      ( y
        ( FirstMatch x 38 )
      )
    )
    ( if
      ( equal x y ) x
      ( erApplyFinalRule y )
    )
  )
)
;---------------------
;
; Degree of match
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote erDegreeMatch )
        ( quote
          (
            (
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def erDegreeMatch lambda
  ( x )
  ( if
    ( erMatch x ) 100
    ( let
      (
        ( t
          ( sub
            ( xComplex x )
            ( xOpr x )
          )
        )
        ( m
          ( xMetaSym x )
        )
      )
      ( pdiv m t )
    )
  )
)
;---------------------
;--------------------------------------------------------------------
; FF model (Finite Function)
;
;         not(xFirstMatch(RX(x),pattern)) &&

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote ffMatch )
        ( quote
          (
            (
              ( X )
            )
            ( SYM )
          )
        )
      )
    )
  )
)
;---------------------

( def ffMatch lambda
  ( x )
  ( let
    (
      ( pattern
        ( O "->"
          ( makeseq 'X 'Y )
        )
      )
    )
    ( and
      ( and
        ( xMatch x pattern )
        ( or
          ( or
            ( is V
              ( RX x )
            )
            ( isC
              ( RX x )
            )
          )
          ( xProdOrio
            ( RX x )
          )
        )
      )
      ( or
        ( or
          ( is V
            ( LX x )
          )
          ( isC
            ( LX x )
          )
        )
        ( xProdOrio
          ( LX x )
        )
      )
    )
  )
)
;---------------------
;
; If ffFirstMatch replaces the expression match with '_ff_
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote ffMetaMatch )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def ffMetaMatch lambda
  ( x1 )
  ( if
    ( ffMatch x1 ) '_ff_
    ( if
      ( and
        ( is O x1 )
        ( equal
          ( OX x1 ) "*"
        )
      )
      ( cond
        (
          ( equal
            ( LX x1 ) '_ff_
          )
          ( O
            ( OX x1 )
            ( makeseq '_ff_
              ( ffMetaMatch
                ( RX x1 )
              )
            )
          )
        )
        (
          ( equal
            ( RX x1 ) '_ff_
          )
          ( O
            ( OX x1 )
            ( makeseq
              ( ffMetaMatch
                ( LX x1 )
              ) '_ff_
            )
          )
        )
        ( true
          ( O
            ( OX x1 )
            ( makeseq
              ( ffMetaMatch
                ( LX x1 )
              )
              ( ffMetaMatch
                ( RX x1 )
              )
            )
          )
        )
      ) x1
    )
  )
)
;---------------------
;
; Applies ffMetaMatch until no more applications are possible
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote ffApplyMetaMatch )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def ffApplyMetaMatch lambda
  ( x )
  ( let
    (
      ( y
        ( ffMetaMatch x )
      )
    )
    ( if
      ( equal x y ) x
      ( ffApplyMetaMatch y )
    )
  )
)
;---------------------
;
; Degree of match
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote ffDegreeMatch )
        ( quote
          (
            (
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def ffDegreeMatch lambda
  ( x )
  ( if
    ( ffMatch x ) 100
    ( let
      (
        ( t
          ( sub
            ( xComplex x )
            ( xOpr x )
          )
        )
        ( m
          ( xMetaSym x )
        )
      )
      ( pdiv m t )
    )
  )
)
;---------------------
;--------------------------------------------------------------------
; FD model (Functional Depedence)
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote fdMatch )
        ( quote
          (
            (
              ( X )
            )
            ( SYM )
          )
        )
      )
    )
  )
)
;---------------------

( def fdMatch lambda
  ( x )
  ( let
    (
      ( pattern
        ( O "->"
          ( makeseq 'X
            ( O "*"
              ( makeseq 'Y 'Z )
            )
          )
        )
      )
    )
    ( and
      ( xMatch x pattern )
      ( xProdOrio
        ( RX x )
      )
    )
  )
)
;---------------------
;
; If fdFirstMatch replaces the expression match with '_fd_
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote fdMetaMatch )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def fdMetaMatch lambda
  ( x1 )
  ( if
    ( fdMatch x1 ) '_fd_
    ( if
      ( and
        ( is O x1 )
        ( equal
          ( OX x1 ) "*"
        )
      )
      ( cond
        (
          ( equal
            ( LX x1 ) '_fd_
          )
          ( O
            ( OX x1 )
            ( makeseq '_fd_
              ( fdMetaMatch
                ( RX x1 )
              )
            )
          )
        )
        (
          ( equal
            ( RX x1 ) '_fd_
          )
          ( O
            ( OX x1 )
            ( makeseq
              ( fdMetaMatch
                ( LX x1 )
              ) '_fd_
            )
          )
        )
        ( true
          ( O
            ( OX x1 )
            ( makeseq
              ( fdMetaMatch
                ( LX x1 )
              )
              ( fdMetaMatch
                ( RX x1 )
              )
            )
          )
        )
      ) x1
    )
  )
)
;---------------------
;
; Applies fdMetaMatch until no more applications are possible
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote fdApplyMetaMatch )
        ( quote
          (
            (
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def fdApplyMetaMatch lambda
  ( x )
  ( let
    (
      ( y
        ( fdMetaMatch x )
      )
    )
    ( if
      ( equal x y ) x
      ( fdApplyMetaMatch y )
    )
  )
)
;---------------------
;
; Degree of match
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote fdDegreeMatch )
        ( quote
          (
            (
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def fdDegreeMatch lambda
  ( x )
  ( if
    ( fdMatch x ) 100
    ( let
      (
        ( t
          ( sub
            ( xComplex x )
            ( xOpr x )
          )
        )
        ( m
          ( xMetaSym x )
        )
      )
      ( pdiv m t )
    )
  )
)
;---------------------