(READMAC ";" (READMAC "?" F))

(DELIM ";" (DELIM "?" F))

(CSETQ MAP2C
(LAMBDA (L1 L2 FN)
        (PROG NIL
           LP <COND [<OR [NULL L1]
                         [NULL L2]> <RETURN NIL>]>
              <FN (CAR L1) (CAR L2)>
              <SETQ L1 (CDR L1)>
              <SETQ L2 (CDR L2)>
              <GO LP>)))

(CSETQ MAPCONC
(LAMBDA (L FN)
        (COND [<NULL L> NIL]
              [T <NCONC (FN (CAR L)) (MAPCONC (CDR L) FN)>])))

(CSETQ PRINTL
(LAMBDA L
        (MAPC L
         (LAMBDA (I)
                 (PRIN1 I)
                 (PRIN1 " ")))
        (TERPRI)
        T))

(CSETQ PROG1
(LAMBDA (X)
        X))

(CSETQ SPACES
(LAMBDA (A)
        (COND [<NOT (LESSP A 1)>
                <PRIN1 " ">
                <SPACES (SUB1 A)>])))

(CSETQ PLNR
(LAMBDA NIL
        (PROG <(THALIST (LIST (LIST NIL NIL)))>
              <CSETQ THINDENT 0>
              <CSETQ THSTEP NIL>
              <CSETQ THSTEPD NIL>
              <CSETQ THSTEPT NIL>
              <CSETQ THSTEPF NIL>
              <CSETQ THTRACEV NIL>
              <BACKTR 1>
              <READMAC "$"
               (LAMBDA NIL
                       (PROG <(THNC (READCH))>
                             <RETURN
                              (COND [<EQ THNC '?>
                                      <LIST 'THV (TOKEN)>]
                                    [<EQ THNC '=>
                                      <LIST 'THNV (TOKEN)>]
                                    [<EQ THNC '&>
                                      <LIST 'THEV (READ)>]
                                    [<EQ THNC 'N>
                                      <LIST 'THANUM (TOKEN)>]
                                    [<DELIM (STRING THNC)>
                                      <BACKSP>
                                      '$]
                                    [<EQ (SETQ THNC
                                       (DO <BACKSP>
                                           <TOKEN>)) 'G> 'THGOAL]
                                    [<EQ THNC 'A> 'THASSERT]
                                    [<EQ THNC 'AL> 'THASSERTLIST]
                                    [<EQ THNC 'E> 'THERASE]
                                    [<EQ THNC 'R> 'THRESTRICT]
                                    [<EQ THNC 'T> '<THTBF THTRUE>]
                                    [<EQ THNC 'V> 'THEV]
                                    [<EQ THNC 'TC> 'THCONSE]
                                    [<EQ THNC 'TA> 'THANTE]
                                    [<EQ THNC 'TE> 'THERASING]
                                    [T <COMPRESS (CONS "$" (EXPLODE THNC
                                        ))>])>))>
              <RETURN (LISP PLNRREAD)>)))

(CSETQ PLNRREAD
(LAMBDA NIL
        (PROG <THFORM>
              <TERPRI>
              <CLEARBUFF>
              <SPACE 1>
              <PRINT "THVAL:">
              <CSETQ THINF F>
              <CSETQ THMESSAGEV NIL>
              <SETQ THFORM (READ)>
              <AND [NOT (ATOM THFORM)]
                   [EQ (CAR THFORM) 'RETURN]
                   [RETURN THFORM]>
              <RETURN (LIST 'THVAL (LIST 'QUOTE THFORM) 'THALIST)>)))

(CSETQ THADD
(LAMBDA (THTT THPL)
        (PROG <THNF THWH THCK THLAS THTTL THT1 THFST THFSTP THFOO>
              <SETQ THCK
               (COND [<ATOM THTT>
                       <OR [SETQ THT1 (GET THTT 'THEOREM)]
                           [DO <PRINT THTT>
                               <THERT
                                "CAN'T THASSERT NO THEOREM - THADD">]>
                       <SETQ THWH (CAR THT1)>
                       <SETQ THTTL THTT>
                       <AND THPL
                            [PROG NIL
                               LP <THPUTPROP THTT (CADR THPL) (CAR THPL)
                                   >
                                  <COND [<SETQ THPL (CDDR THPL)> <GO LP>
                                         ]>]>
                       <CADDR THT1>]
                     [T <SETQ THWH 'THASSERTION>
                        <SETQ THTTL (CONS THTT THPL)>
                        THTT])>
              <SETQ THNF 0>
              <SETQ THLAS (LENGTH THCK)>
              <SETQ THFST T>
         THP1 <COND [<NULL THCK>
                      <SETQ THCK THFOO>
                      <SETQ THNF 0>
                      <SETQ THFOO (SETQ THFST NIL)>
                      <SETQ THFSTP T>
                      <GO THP1>]
                    [<NULL (SETQ THT1 (THIP (CAR THCK)))> <RETURN NIL>]
                    [<EQ THT1 'THOK>]
                    [<SETQ THFOO (NCONC THFOO (LIST
                       (COND [<EQ THT1 'THVRB> <CAR THCK>])))>
                      <SETQ THCK (CDR THCK)>
                      <GO THP1>]>
              <SETQ THFST NIL>
              <MAPC (CDR THCK) THIP>
              <SETQ THNF 0>
              <MAPC THFOO THIP>
              <RETURN THTTL>)))

(DEFSPEC THAMONG
(LAMBDA THA
        (COND [<EQ (CADR (CSETQ THXX (THGAL
                 (COND [<EQ (CAAR THA) 'THEV>
                         <THVAL (CADAR THA) THALIST>]
                       [T <CAR THA>]) THALIST))) 'THUNASSIGNED>
                <THPUSH THTREE (LIST 'THAMONG THXX (THVAL (CADR THA)
                 THALIST))>
                NIL]
              [T <MEMBER (CADR THXX) (THVAL (CADR THA) THALIST)>])))

(CSETQ THAMONGF
(LAMBDA NIL
        (COND [THMESSAGEV
                <THPOPT>
                NIL]
              [<CADDAR THTREE>
                <RPLACA (CDADAR THTREE) (CAADDAR THTREE)>
                <RPLACA (CDDAR THTREE) (CDADDAR THTREE)>
                <SETQ THBRANCHV THTREE>
                <SETQ THABRANCH THALIST>
                <THPOPT>
                T]
              [T <RPLACA (CDADAR THTREE) 'THUNASSIGNED>
                 <THPOPT>
                 NIL])))

(DEFSPEC THAND
(LAMBDA A
        (OR [NOT A]
            [DO <THPUSH THTREE (LIST 'THAND A NIL)>
                <SETQ THEXP (CAR A)>])))

(CSETQ THANDF
(LAMBDA NIL
        (THBRANCHUN)
        NIL))

(CSETQ THANDT
(LAMBDA NIL
        (COND [<CDADAR THTREE>
                <THBRANCH>
                <SETQ THEXP (CADADAR THTREE)>
                <RPLACA (CDAR THTREE) (CDADAR THTREE)>]
              [<THPOPT>])
        THVALUE))

(DEFSPEC THANTE
(LAMBDA THX
        (THDEF 'THANTE THX)))

(DEFSPEC THAPPLY
(LAMBDA (THM DAT)
        (THAPPLY1 THM (GET THM 'THEOREM) DAT)))

(CSETQ THAPPLY1
(LAMBDA (THM THB DAT)
        (COND [<AND [THBIND (CADR THB)]
                    [THMATCH1 DAT (CADDR THB)]>
                <AND THTRACEV
                     [THTRACES 'THEOREM THM]>
                <THPUSH THTREE '(THEOREM)>
                <THPUSH THTREE (LIST 'THPROG (CDDR THB) NIL (CDDR THB))>
                <THPROGA>
                T]
              [T <SETQ THALIST THOLIST>
                 <THPOPT>
                 NIL])))

(CSETQ THASS1
(LAMBDA (THA P)
        (PROG <THX THY1 THY TYPE PSEUDO>
              <AND [CDR THA]
                   [CADR THA]
                   [EQ (CAADR THA) 'THPSEUDO]
                   [SETQ PSEUDO T]>
              <OR [ATOM (SETQ THX (CAR THA))]
                  [THPURE (SETQ THX (THVARSUBST THX NIL))]
                  PSEUDO
                  [DO <PRINT THX>
                      <THERT "IMPURE ASSERTION OR ERASURE - THASS1">]>
              <AND THTRACEV
                   [THTRACES
                    (COND [P 'THASSERT]
                          ['THERASE]) THX]>
              <SETQ THA
               (COND [PSEUDO <CDDR THA>]
                     [<CDR THA>])>
              <OR [SETQ THX
                   (COND [PSEUDO <LIST THX>]
                         [P <THADD THX (SETQ THY
                             (COND [<AND THA
                                         [EQ (CAAR THA) 'THPROP]>
                                     <PROG1 (EVAL (CADAR THA)) (SETQ THA
                                      (CDR THA))>]))>]
                         [T <THREMOVE THX>])]
                  [RETURN NIL]>
              <COND [P <SETQ TYPE 'THANTE>]
                    [T <SETQ TYPE 'THERASING>]>
              <OR PSEUDO
                  [THPUSH THTREE (LIST
                   (COND [P 'THASSERT]
                         [T 'THERASE]) THX THY)]>
              <SETQ THY (MAPCONC THA THTAE)>
              <COND [THY <SETQ THEXP (CONS 'THDO THY)>]>
              <RETURN THX>)))

(DEFSPEC THASSERT
(LAMBDA THA
        (THASS1 THA T)))
(DEFMAC THASSERTLIST
(LAMBDA (THA . THRECS)
        (PROG <THA1>
              <SETQ THA1 (CAR (NTH THA -1))>
              <SETQ THA (REVERSE (CDR (REVERSE THA)))>
              <RETURN (CONS 'THDO (MAPCAR THA1
               (LAMBDA (THA2)
                       (LIST 'THASSERT (APPEND THA (LIST THA2)) (STACK
                        THRECS)))))>)))

(CSETQ THASSERTF
(LAMBDA NIL
        (THREMOVE
         (COND [<ATOM (CADAR THTREE)> <CADAR THTREE>]
               [T <CAADAR THTREE>]))
        (THPOPT)
        NIL))

(CSETQ THASSERTT
(LAMBDA NIL
        (PROG1 (CADAR THTREE) (THPOPT))))

(DEFSPEC THASVAL
(LAMBDA (X)
        (AND [SETQ X (THSGAL X)]
             [NOT (EQ (CADR X) 'THUNASSIGNED)])))

(CSETQ THBAP
(LAMBDA (TH1 TH2)
        (PROG <THP>
              <SETQ THP TH2>
         THP1 <AND [EQUAL
                    (COND [THPC <CADR THP>]
                          [T <CAADR THP>]) TH1]
                   [RETURN THP]>
              <OR [CDR (SETQ THP (CDR THP))]
                  [RETURN NIL]>
              <GO THP1>)))

(CSETQ THBI1
(LAMBDA (X)
        (COND [<ATOM X> <LIST X 'THUNASSIGNED>]
              [T <LIST (CAR X) (EVAL (CADR X))>])))

(CSETQ THBIND
(LAMBDA (A)
        (SETQ THOLIST THALIST)
        (OR [NULL A]
            [PROG NIL
               GO <COND [<NULL A>
                          <THPUSH THTREE (LIST 'THREMBIND THOLIST)>
                          <RETURN T>]>
                  <THPUSH THALIST
                   (COND [<ATOM (CAR A)>
                           <LIST (CAR A) 'THUNASSIGNED>]
                         [<EQ (CAAR A) 'THRESTRICT>
                           <NCONC (THBI1 (CADAR A)) (CDDAR A)>]
                         [T <LIST (CAAR A) (EVAL (CADAR A))>])>
                  <SETQ A (CDR A)>
                  <GO GO>])))

(CSETQ THBRANCH
(LAMBDA NIL
        (COND [<NOT (CDADAR THTREE)>]
              [<EQ THBRANCHV THTREE> <SETQ THBRANCHV NIL>]
              [<RPLACA (CDDAR THTREE) (CONS (LIST THBRANCHV THABRANCH (
                 CADAR THTREE)) (CADDAR THTREE))> <SETQ THBRANCHV NIL>])
))

(CSETQ THBRANCHUN
(LAMBDA NIL
        (PROG <X>
              <RETURN
               (COND [<SETQ X (CADDAR THTREE)>
                       <RPLACA (CDAR THTREE) (CADDAR X)>
                       <RPLACA (CDDAR THTREE) (CDR X)>
                       <SETQ THALIST (CADAR X)>
                       <SETQ THTREE (CAAR X)>
                       T]
                     [T <THPOPT>
                        NIL])>)))

(CSETQ THCHECK
(LAMBDA (THPRD THX)
        (OR [NULL THPRD]
            [EQ THX 'THUNASSIGNED]
            [ATTEMPT [DO <MAPC THPRD
                          (LAMBDA (THY)
                                  (OR [(EVAL THY) THX]
                                      [ERROR 1]))>
                         T]
                     [1 F]])))

(DEFSPEC THCOND
(LAMBDA THA
        (THPUSH THTREE (LIST 'THCOND THA NIL))
        (SETQ THEXP (CAAR THA))))

(CSETQ THCONDF
(LAMBDA NIL
        (THOR2 NIL)))

(CSETQ THCONDT
(LAMBDA NIL
        (RPLACA (CAR THTREE) 'THAND)
        (RPLACA (CDAR THTREE) (CAADAR THTREE))
        THVALUE))

(DEFSPEC THCONSE
(LAMBDA THX
        (THDEF 'THCONSE THX)))

(CSETQ THDATA
(LAMBDA NIL
        (PROG <X>
              <TERPRI>
           GO <COND [<ATOM (SETQ X (READ))> <RETURN X>]
                    [<THADD (CAR X) (CDR X)> <PRINT X>]
                    [T <PRIN1 X>
                       <PRINT " ALREADY ASSERTED">]>
              <GO GO>)))

(CSETQ THDEF
(LAMBDA (THMTYPE THX)
        (PROG <THNOASSERT? THMNAME THMBODY>
              <COND [<NOT (ATOM (CAR THX))>
                      <SETQ THMBODY THX>
                      <COND [<EQ THMTYPE 'THCONSE>
                              <SETQ THMNAME (THGENSYM 'TC-G)>]
                            [<EQ THMTYPE 'THANTE>
                              <SETQ THMNAME (THGENSYM 'TA-G)>]
                            [<EQ THMTYPE 'THERASING>
                              <SETQ THMNAME (THGENSYM 'TE-G)>]
                            [T <PRINT THMTYPE>
                               <THERT "UNKNOWN THEOREM TYPE - THDEF">]>]
                    [<SETQ THMNAME (CAR THX)> <SETQ THMBODY (CDR THX)>]>
              <COND [<EQ (CAR THMBODY) 'THNOASSERT>
                      <SETQ THNOASSERT? T>
                      <SETQ THMBODY (CDR THMBODY)>]>
              <THPUTPROP THMNAME (CONS THMTYPE THMBODY) 'THEOREM>
              <COND [THNOASSERT?
                      <PRINTL THMNAME "DEFINED BUT NOT ASSERTED">
                      <RETURN THMNAME>]
                    [<THASS1 (LIST THMNAME) T>
                      <PRINTL THMNAME "DEFINED AND ASSERTED">
                      <RETURN THMNAME>]
                    [T <PRINTL THMNAME "REDEFINED">
                       <RETURN THMNAME>]>)))

(DEFSPEC THDO
(LAMBDA A
        (OR [NOT A]
            [DO <THPUSH THTREE (LIST 'THDO A NIL NIL)>
                <SETQ THEXP (CAR A)>])))

(CSETQ THDOB
(LAMBDA NIL
        (COND [<OR THMESSAGEV
                   [NULL (CDADAR THTREE)]>
                <RPLACA (CAR THTREE) 'THUNDO>
                T]
              [<THDO1>])))

(CSETQ THDO1
(LAMBDA NIL
        (RPLACA (CDAR THTREE) (CDADAR THTREE))
        (SETQ THEXP (CAADAR THTREE))
        (COND [THBRANCHV
                <RPLACA (CDDAR THTREE) (CONS THBRANCHV (CADDAR THTREE))>
                <SETQ THBRANCHV NIL>
                <RPLACA (CDDDAR THTREE) (CONS THABRANCH (CADDDAR THTREE)
                 )>])))

(CSETQ THDUMP
(LAMBDA THFILE
        (PROG <L>
              <OBLIST
               (LAMBDA (A)
                       (COND [<GET A 'THEOREM> <SETQ L (CONS A L)>]))>
              <TERPRI (STACK THFILE)>
              <PRINT "(DO">
              <THPRETTYP L (STACK THFILE)>
              <PRINT "(THDATA))">
              <THSTATE>
              <PRINT "LOADED">
              <TERPRI>
              <RETURN "DUMPED">)))

(DEFSPEC THERASE
(LAMBDA THA
        (THASS1 THA NIL)))

(CSETQ THERASEF
(LAMBDA NIL
        (THADD
         (COND [<ATOM (CADAR THTREE)> <CADAR THTREE>]
               [T <CAADAR THTREE>])
         (COND [<ATOM (CADAR THTREE)> NIL]
               [T <CDADAR THTREE>]))
        (THPOPT)
        NIL))

(CSETQ THERASET
(LAMBDA NIL
        (PROG1 (CADAR THTREE) (THPOPT))))

(DEFSPEC THERASING
(LAMBDA THX
        (THDEF 'THERASING THX)))

(DEFSPEC THERT
(LAMBDA (L)
        (TERPRI)
        (CLEARBUFF)
        (PRINT L)
        (CSETQ THINF T)
        (ERROR 0)))

(DEFSPEC THEV
(LAMBDA (THA)
        (THVAL THA THALIST)))

(DEFSPEC THFAIL
(LAMBDA THA
        (AND THA
             [PROG <THTREE1 THA1 THX>
                   <SETQ THTREE1 THTREE>
                   <SETQ THA1
                    (COND [<EQ (CAR THA) 'THTAG> 'THPROG]
                          [<EQ (CAR THA) 'THINF>
                            <CSETQ THINF T>
                            <RETURN NIL>]
                          [<EQ (CAR THA) 'THMESSAGE>
                            <CSETQ THMESSAGEV (THVARSUBST (CADR THA) NIL
                             )>
                            <RETURN NIL>]
                          [T <CAR THA>])>
               LP1 <COND [<NULL THTREE1>
                           <PRINT THA>
                           <THERT "NOT FOUND - THFAIL">]
                         [<EQ (CAAR THTREE1) THA1> <GO ELP1>]>
              ALP1 <SETQ THTREE1 (CDR THTREE1)>
                   <GO LP1>
              ELP1 <COND [<EQ (CAR THA) 'THTAG>
                           <COND [<MEMBER (CADR THA) (CADDDAR THTREE1)>
                                   <GO TAGS>]
                                 [T <GO ALP1>]>]>
                   <CSETQ THMESSAGEV (LIST (CDR THTREE1)
                    (AND [CDR THA]
                         [CADR THA]))>
                   <RETURN NIL>
              TAGS <SETQ THX (CADDAR THTREE1)>
               LP2 <COND [<NULL (CAR THX)> <GO ALP1>]
                         [<EQ (CAADDAR THX) (CADR THA)>
                           <CSETQ THMESSAGEV (LIST (CAAR THX)
                            (AND [CDDR THA]
                                 [CADDR THA]))>
                           <RETURN NIL>]>
                   <SETQ THX (CDR THX)>
                   <GO LP2>])))

(CSETQ THFAIL?
(LAMBDA (PRD ACT)
        (THPUSH THTREE (LIST 'THFAIL? PRD ACT))
        THVALUE))

(CSETQ THFAIL?F
(LAMBDA NIL
        (COND [<EVAL (CADAR THTREE)>
                <(LAMBDA (X Y)
                         Y) (CSETQ THMESSAGEV NIL) (EVAL (CADDAR THTREE)
                 ) (THPOPT)>]
              [T <THPOPT>
                 NIL])))

(DEFSPEC THFINALIZE
(LAMBDA THA
        (PROG <THTREE1 THT THX>
              <COND [<NULL THA> <THERT "NULL ARGUMENT - THFINALIZE">]
                    [<EQ (CAR THA) 'THTAG> <SETQ THT (CADR THA)>]>
              <SETQ THTREE (SETQ THTREE1 (CONS NIL THTREE))>
         PLUP <AND [NULL (SETQ THX (CDR THTREE1))]
                   [PRINT THA]
                   [THERT "OVERPOP - THFINALIZE"]>
              <SETQ THX (CAR THX)>
              <COND [<AND THT
                          [EQ (CAR THX) 'THPROG]
                          [MEMBER THT (CADDDR THX)]> <GO RTLEV>]
                    [<OR [EQ (CAR THX) 'THPROG]
                         [EQ (CAR THX) 'THAND]>
                      <RPLACA (CDDR THX) NIL>
                      <SETQ THTREE1 (CDR THTREE1)>]
                    [<EQ (CAR THX) 'THREMBIND>
                      <SETQ THTREE1 (CDR THTREE1)>]
                    [<RPLACD THTREE1 (CDDR THTREE1)>]>
              <COND [<EQ (CAR THX) (CAR THA)> <GO DONE>]>
              <GO PLUP>
        RTLEV <SETQ THX (CDDR THX)>
        LEVLP <COND [<NULL (CAR THX)>
                      <SETQ THTREE1 (CDR THTREE1)>
                      <GO PLUP>]
                    [<EQ (CAADDAAR THX) THT> <GO DONE>]>
              <RPLACA THX (CDAR THX)>
              <GO LEVLP>
         DONE <THPOPT>
              <RETURN T>)))

(DEFSPEC THFIND
(LAMBDA THA
        (THBIND (CADDR THA))
        (THPUSH THTREE (LIST 'THFIND
         (COND [<EQ (CAR THA) 'ALL> 'ə NIL NIL>]
               [<NUMBERP (CAR THA)> <LIST (CAR THA) (CAR THA) T>]
               [<NUMBERP (CAAR THA)> <CAR THA>]
               [<EQ (CAAR THA) 'EXACTLY>
                 <LIST (CADAR THA) (ADD1 (CADAR THA)) NIL>]
               [<EQ (CAAR THA) 'AT-MOST> <LIST 1 (ADD1 (CADAR THA)) NIL>
                ]
               [<EQ (CAAR THA) 'AS-MANY-AS> <LIST 1 (CADAR THA) T>]
               [T <CONS (CADAR THA)
                   (COND [<NULL (CDDAR THA)> <LIST NIL T>]
                         [<EQ (CADDAR THA) 'AT-MOST>
                           <LIST (ADD1 (CADDDAR THA)) NIL>]
                         [T <LIST (CADDDAR THA) T>])>]) (CONS 0 NIL) (
         CADR THA)))
        (THPUSH THTREE (LIST 'THPROG (CDDR THA) NIL (CDDR THA)))
        (THPROGA)))

(CSETQ THFINDF
(LAMBDA NIL
        (SETQ THBRANCHV NIL)
        (COND [<OR THMESSAGEV
                   [LESSP (CAADR (CSETQ THXX (CDAR THTREE))) (CAAR THXX)
                    ]>
                <THPOPT>
                NIL]
              [T <THPOPT>
                 <CDADR THXX>])))

(CSETQ THFINDT
(LAMBDA NIL
        (PROG <THX THY THZ THCDAR>
              <SETQ THZ (CADDR (SETQ THCDAR (CDAR THTREE)))>
              <AND [MEMBER (SETQ THX (THVARSUBST THZ NIL)) (CDADR THCDAR
                    )]
                   [GO GO]>
              <RPLACD (CADR THCDAR) (CONS THX (CDADR THCDAR))>
              <AND [EQUAL (SETQ THY (ADD1 (CAADR THCDAR))) (CADAR THCDAR
                    )]
                   [RETURN (PROG1
                    (AND [CADDAR THCDAR]
                         [CDADR THCDAR]) (SETQ THBRANCHV NIL) (THPOPT))]
               >
              <RPLACA (CADR THCDAR) THY>
           GO <SETQ THTREE THBRANCHV>
              <SETQ THALIST THABRANCH>
              <SETQ THBRANCHV NIL>
              <RETURN NIL>)))

(DEFSPEC THFLUSH
(LAMBDA INDS
        (SETQ INDS
         (OR INDS
             '[THASSERTION THCONSE THANTE THERASING]))
        (OBLIST
         (LAMBDA (AT)
                 (MAPC INDS
                  (LAMBDA (P)
                          (REMPROP AT P)))))
        "DONE"))

(CSETQ THGAL
(LAMBDA (X Y)
        (CSETQ THXX X)
        (OR [ASSOC (CADR X) Y]
            [DO <PRINT THXX>
                <THERT "THUNBOUND - THGAL">])))

(CSETQ THGENSYM
(LAMBDA (X)
        (COMPRESS (EXPLODE (GENSYM X)))))

(DEFMAC THGO
(LAMBDA (X)
        (LIST 'THSUCCEED 'THTAG X)))

(DEFSPEC THGOAL
(LAMBDA THA
        (PROG <THY THY1 THZ THZ1 THA1 THA2>
              <SETQ THA2 (THVARSUBST (CAR THA) T)>
              <SETQ THA1 (CDR THA)>
              <COND [<OR [NULL THA1]
                         [AND [NOT (AND [EQ (CAAR THA1) 'THANUM]
                                        [SETQ THA1 (CONS (LIST 'THNUM (
                                         CADAR THA1)) (CONS '(THDBF
                                         THTRUE) (CDR THA1)))])]
                              [NOT (AND [EQ (CAAR THA1) 'THNODB]
                                        [DO <SETQ THA1 (CDR THA1)>
                                            T])]
                              [NOT (EQ (CAAR THA1) 'THDBF)]]>
                      <SETQ THA1 (CONS '(THDBF THTRUE) THA1)>]>
              <SETQ THA1 (MAPCONC THA1 THTRY)>
              <AND THTRACEV
                   [THTRACES 'THGOAL THA2]>
              <COND [<NULL THA1> <RETURN NIL>]>
              <THPUSH THTREE (LIST 'THGOAL THA2 THA1)>
              <RPLACD (CDDAR THTREE) 777777Q>
              <RETURN NIL>)))

(CSETQ THGOALF
(LAMBDA NIL
        (COND [THMESSAGEV
                <THPOPT>
                NIL]
              [<THTRY1>]
              [T <THPOPT>
                 NIL])))

(CSETQ THGOALT
(LAMBDA NIL
        (PROG1
         (COND [<EQ THVALUE 'THNOVAL>
                 <LIST (THVARSUBST (CADAR THTREE) NIL)>]
               [THVALUE]) (THPOPT))))

(CSETQ THIP
(LAMBDA (THI)
        (PROG <THT1 THT3 THSV THT2 THI1>
              <SETQ THNF (ADD1 THNF)>
              <COND [<NUMBERP THI> <RETURN 'THVRB>]
                    [<AND [ATOM THI]
                          [NOT (EQ THI '?)]> <SETQ THI1 THI>]
                    [<OR [EQ THI '?]
                         [MEMBER (CAR THI) '(THV THNV)]>
                      <COND [THFST <RETURN 'THVRB>]
                            [<SETQ THI1 'THVRB>]>]
                    [<RETURN 'THVRB>]>
              <COND [<NOT (SETQ THT1 (GET THI1 THWH))>
                      <PUT THI1 THWH (LIST NIL (LIST THNF (LIST THLAS 1
                       THTTL)))>]
                    [<EQ THT1 'THNOHASH> <RETURN 'THBQF>]
                    [<NOT (SETQ THT2 (ASSOC THNF (CDR THT1)))>
                      <NCONC THT1 (LIST (LIST THNF (LIST THLAS 1 THTTL))
                       )>]
                    [<NOT (SETQ THT3 (ASSOC THLAS (CDR THT2)))>
                      <NCONC THT2 (LIST (LIST THLAS 1 THTTL))>]
                    [<AND [OR THFST
                              THFSTP]
                          [COND [<EQ THWH 'THASSERTION>
                                  <ASSOC THTT (CDDR THT3)>]
                                [T <MEMBER THTT (CDDR THT3)>]]>
                      <RETURN NIL>]
                    [<SETQ THSV (CDDR THT3)>
                      <RPLACA (CDR THT3) (ADD1 (CADR THT3))>
                      <RPLACD (CDR THT3) (NCONC (LIST THTTL) THSV)>]>
              <RETURN 'THOK>)))

(CSETQ THMATCH
(LAMBDA THX
        ((LAMBDA (THOLIST THALIST)
                 (THMATCH1 (CAR THX) (CADR THX)))
         (COND [<GREATERP (LENGTH THX) 2> <CADDR THX>]
               [T THALIST])
         (COND [<GREATERP (LENGTH THX) 3> <CADDDR THX>]
               [T THALIST]))))

(CSETQ THMATCH1
(LAMBDA (THX THY)
        (PROG <THML>
              <COND [<AND [EQUAL (LENGTH
                           (COND [<EQ (CAR THX) 'THEV>
                                   <SETQ THX (THVAL (CADR THX) THOLIST)>
                                  ]
                                 [THX])) (LENGTH THY)]
                          [ATTEMPT [DO <MAP2C THX THY THMATCH2>
                                       T]
                                   [1 F]]>
                      <AND THML
                           [THPUSH THTREE (LIST 'THMUNG THML)]>
                      <RETURN T>]
                    [T <MAPC THML EVAL>
                       <RETURN NIL>]>)))

(CSETQ THMATCH2
(LAMBDA (THX THY)
        (AND [NOT (ATOM THX)]
             [EQ (CAR THX) 'THEV]
             [SETQ THX (THVAL (CADR THX) THOLIST)])
        (AND [NOT (ATOM THY)]
             [EQ (CAR THY) 'THEV]
             [SETQ THY (THVAL (CADR THY) THALIST)])
        (COND [<EQ THX '?>]
              [<EQ THY '?>]
              [<OR [AND [NOT (ATOM THX)]
                        [MEMBER (CAR THX) '(THV THNV THRESTRICT)]]
                   [AND [NOT (ATOM THY)]
                        [MEMBER (CAR THY) '(THV THNV THRESTRICT)]]>
                <(LAMBDA (XPAIR YPAIR)
                         (COND [<AND XPAIR
                                     [OR [EQ (CAR THX) 'THNV]
                                         [AND [EQ (CAR THX) 'THV]
                                              [EQ (CADR XPAIR) '
                                               THUNASSIGNED]]]
                                     [THCHECK (CDDR XPAIR)
                                      (COND [YPAIR <CADR YPAIR>]
                                            [T THY])]>
                                 <COND [YPAIR <THRPLACAS (CDR XPAIR) (
                                               CADR YPAIR)>

     <AND [CDDR YPAIR]
          [THRPLACDS (CDR XPAIR) (THUNION (CDDR XPAIR) (CDDR YPAIR))]>
                                              <THRPLACDS YPAIR (CDR
                                               XPAIR)>]
                                       [T <THRPLACAS (CDR XPAIR) THY>]>]
                               [<AND YPAIR
                                     [OR [EQ (CAR THY) 'THNV]
                                         [AND [EQ (CAR THY) 'THV]
                                              [EQ (CADR YPAIR) '
                                               THUNASSIGNED]]]
                                     [THCHECK (CDDR YPAIR)
                                      (COND [XPAIR <CADR XPAIR>]
                                            [T THX])]>
                                 <COND [XPAIR <THRPLACAS (CDR YPAIR) (
                                               CADR XPAIR)>]
                                       [T <THRPLACAS (CDR YPAIR) THX>]>]
                               [<AND XPAIR
                                     [EQUAL (CADR XPAIR)
                                      (COND [YPAIR <CADR YPAIR>]
                                            [T THY])]>]
                               [<AND YPAIR
                                     [EQUAL (CADR YPAIR) THX]>]
                               [T <ERROR 1>]))
                 (COND [<THVAR THX> <THGAL THX THOLIST>]
                       [<AND [NOT (ATOM THX)]
                             [EQ (CAR THX) 'THRESTRICT]>
                         <COND [<EQ (CADR THX) '?>
                                 <PROG1 (CONS '? (CONS 'THUNASSIGNED (
                                  APPEND (CDDR THX) NIL))) (SETQ THX '(
                                  THNV ?))>]
                               [T <(LAMBDA (U)
                                           (THRPLACDS (CDR U) (THUNION (
                                            CDDR U) (CDDR THX)))
                                           (SETQ THX (CADR THX))
                                           U) (THGAL (CADR THX) THOLIST)
                                   >]>])
                 (COND [<THVAR THY> <THGAL THY THALIST>]
                       [<AND [NOT (ATOM THY)]
                             [EQ (CAR THY) 'THRESTRICT]>
                         <COND [<EQ (CADR THY) '?>
                                 <PROG1 (CONS '? (CONS 'THUNASSIGNED (
                                  APPEND (CDDR THY) NIL))) (SETQ THY '(
                                  THNV ?))>]
                               [T <(LAMBDA (U)
                                           (THRPLACDS (CDR U) (THUNION (
                                            CDDR U) (CDDR THY)))
                                           (SETQ THY (CADR THY))
                                           U) (THGAL (CADR THY) THALIST)
                                   >]>])>]
              [<EQUAL THX THY>]
              [T <ERROR 1>])))

(CSETQ THMATCHLIST
(LAMBDA (THTB THWH)
        (PROG <THB1 THB2 THL THNF THAL THA1 THA2 THRN THL1 THL2 THRVC>
              <SETQ THL 377777777777Q>
              <SETQ THNF 0>
              <SETQ THAL (LENGTH THTB)>
              <SETQ THB1 THTB>
         THP1 <OR THB1
                  [RETURN
                   (COND [THL2 <APPEND THL1 THL2>]
                         [THL1])]>
              <SETQ THNF (ADD1 THNF)>
              <SETQ THB2 (CAR THB1)>
              <SETQ THB1 (CDR THB1)>
         THP3 <COND [<OR [NULL (ATOM THB2)]
                         [NUMBERP THB2]
                         [EQ THB2 '?]> <GO THP1>]
                    [<NOT (SETQ THA1 (GET THB2 THWH))>
                      <SETQ THA1 '(0 0)>]
                    [<EQ THA1 'THNOHASH> <GO THP1>]
                    [<NOT (SETQ THA1 (ASSOC THNF (CDR THA1)))>
                      <SETQ THA1 '(0 0)>]
                    [<NOT (SETQ THA1 (ASSOC THAL (CDR THA1)))>
                      <SETQ THA1 '(0 0)>]>
              <SETQ THRN (CADR THA1)>
              <SETQ THA1 (CDDR THA1)>
              <AND [EQ THWH 'THASSERTION]
                   [GO THP2]>
              <COND [<NOT (SETQ THA2 (GET 'THVRB THWH))>
                      <SETQ THA2 '(0 0)>]
                    [<NOT (SETQ THA2 (ASSOC THNF (CDR THA2)))>
                      <SETQ THA2 '(0 0)>]
                    [<NOT (SETQ THA2 (ASSOC THAL (CDR THA2)))>
                      <SETQ THA2 '(0 0)>]>
              <SETQ THRVC (CADR THA2)>
              <SETQ THA2 (CDDR THA2)>
              <AND [GREATERP (PLUS THRVC THRN) THL]
                   [GO THP1]>
              <SETQ THL (PLUS THRVC THRN)>
              <SETQ THL1 THA1>
              <SETQ THL2 THA2>
              <GO THP1>
         THP2 <COND [<ZEROP THRN> <RETURN NIL>]
                    [<GREATERP THL THRN>
                      <SETQ THL1 THA1>
                      <SETQ THL THRN>]>
              <GO THP1>)))

(DEFSPEC THMESSAGE
(LAMBDA THA
        (THPUSH THTREE (CONS 'THMESSAGE THA))
        THVALUE))

(CSETQ THMESSAGEF
(LAMBDA NIL
        (PROG <BOD>
              <SETQ BOD (CAR THTREE)>
              <THPOPT>
              <COND [<AND [THBIND (CADR BOD)]
                          [THMATCH1 THMESSAGEV (CADDR BOD)]>
                      <THPUSH THTREE (LIST 'THPROG (CDDR BOD) NIL (CDDR
                       BOD))>
                      <CSETQ THMESSAGEV NIL>
                      <RETURN (THPROGA)>]
                    [T <SETQ THALIST THOLIST>]>
              <RETURN NIL>)))

(CSETQ THMUNGF
(LAMBDA NIL
        (MAPC (CADAR THTREE) EVAL)
        (THPOPT)
        NIL))

(CSETQ THNOFAIL
(LAMBDA (THX)
        (COND [THX <PUT 'THPROG 'THFAIL THPROGT>]
              [T <PUT 'THPROG 'THFAIL THPROGF>])))

(DEFSPEC THNOHASH
(LAMBDA (THA . INDS)
        (MAPC (OR INDS
                  '[THASSERTION THCONSE THANTE THERASING])
         (LAMBDA (X)
                 (PUT THA X 'THNOHASH)))))

(DEFMAC THNOT
(LAMBDA (THA)
        (LIST 'THCOND (LIST THA '(THFAIL THAND)) '((THSUCCEED)))))

(DEFSPEC THNV
(LAMBDA (X)
        (THV1 X)))

(DEFSPEC THOR
(LAMBDA THA
        (AND THA
             [THPUSH THTREE (LIST 'THOR THA)]
             [SETQ THEXP (CAR THA)])))

(CSETQ THORF
(LAMBDA NIL
        (THOR2 T)))

(CSETQ THOR2
(LAMBDA (P)
        (COND [THMESSAGEV
                <THPOPT>
                NIL]
              [<AND [CADAR THTREE]
                    [CDADAR THTREE]>
                <RPLACA (CDAR THTREE) (CDADAR THTREE)>
                <SETQ THEXP
                 (COND [P <PROG1 (CAADAR THTREE)
                           (OR [CADAR THTREE]
                               [THPOPT])>]
                       [<CAAADAR THTREE>])>]
              [T <THPOPT>
                 NIL])))

(DEFMAC THPOPT
(LAMBDA NIL
        '(SETQ THTREE (CDR THTREE))))

(CSETQ THPOPTV
(LAMBDA NIL
        (THPOPT)
        THVALUE))

(DEFSPEC THPROG
(LAMBDA THA
        (THBIND (CAR THA))
        (THPUSH THTREE (LIST 'THPROG THA NIL THA))
        (THPROGA)))

(CSETQ THPROGA
(LAMBDA NIL
        ((LAMBDA (X)
                 (COND [<NULL (CDAR X)>
                         <THPOPT>
                         'THNOVAL]
                       [<ATOM (CADAR X)>
                         <SETQ THEXP (LIST 'THTAG (CADAR X))>
                         <RPLACA X (CDAR X)>
                         THVALUE]
                       [T <SETQ THEXP (CADAR X)>
                          <RPLACA X (CDAR X)>
                          THVALUE])) (CDAR THTREE))))

(CSETQ THPROGF
(LAMBDA NIL
        (THBRANCHUN)
        NIL))

(CSETQ THPROGT
(LAMBDA NIL
        (THBRANCH)
        (THPROGA)))

(CSETQ THPURE
(LAMBDA (XX)
        (ATTEMPT [DO <MAPC XX
                      (LAMBDA (Y)
                              (AND [THVAR Y]
                                   [ERROR 1]))>
                     T]
                 [1 F])))

(DEFMAC THPUSH
(LAMBDA (TH1 TH2)
        (LIST 'SETQ TH1 (LIST 'CONS TH2 TH1))))

(CSETQ THPUT
(LAMBDA (ATO IND VAL)
        (THPUSH THTREE (LIST 'THMUNG (LIST (LIST 'PUT (LIST 'QUOTE ATO)
         (LIST 'QUOTE IND) (LIST 'QUOTE (GET ATO IND))))))
        (PUT ATO IND VAL)))

(DEFMAC THPUTPROP
(LAMBDA (ATO VAL IND)
        (LIST 'THPUT ATO IND VAL)))

(CSETQ THREM1
(LAMBDA (THB)
        (PROG <THA THSV THA1 THA2 THA3 THA4 THA5 THONE THPC>
              <SETQ THNF (ADD1 THNF)>
              <COND [<NUMBERP THB> <RETURN 'THVRB>]
                    [<AND [ATOM THB]
                          [NOT (EQ THB '?)]> <SETQ THA THB>]
                    [<OR [EQ THB '?]
                         [MEMBER (CAR THB) '(THV THNV)]>
                      <COND [THFST <RETURN 'THVRB>]
                            [<SETQ THA 'THVRB>]>]
                    [<RETURN 'THVRB>]>
              <OR [SETQ THA1 (GET THA THWH)]
                  [RETURN NIL]>
              <AND [EQ THA1 'THNOHASH]
                   [RETURN 'THBQF]>
              <OR [SETQ THA2 (THBAP THNF THA1)]
                  [RETURN NIL]>
              <OR [SETQ THA3 (THBAP THAL (CADR THA2))]
                  [RETURN NIL]>
              <SETQ THA4 (CADR THA3)>
              <SETQ THPC (NOT (EQ THWH 'THASSERTION))>
              <SETQ THA5
               (COND [<OR THFST
                          THFSTP> <THBAP THBS (CDR THA4)>]
                     [<THBAP (COND [THPC THON]
                                   [T <CAR THON>]) (CDR THA4)>])>
              <OR THA5
                  [RETURN NIL]>
              <SETQ THONE (CADR THA5)>
              <RPLACD THA5 (CDDR THA5)>
              <AND [NOT (EQUAL (CADR THA4) 1)]
                   [OR [SETQ THSV (CDDR THA4)]
                       T]
                   [RPLACA (CDR THA4) (SUB1 (CADR THA4))]
                   [RETURN THONE]>
              <SETQ THSV (CDDR THA3)>
              <RPLACD THA3 THSV>
              <AND [CDADR THA2]
                   [RETURN THONE]>
              <SETQ THSV (CDDR THA2)>
              <RPLACD THA2 THSV>
              <AND [CDR THA1]
                   [RETURN THONE]>
              <REMPROP THA THWH>
              <RETURN THONE>)))

(CSETQ THREMBINDF
(LAMBDA NIL
        (SETQ THALIST (CADAR THTREE))
        (THPOPT)
        NIL))

(CSETQ THREMBINDT
(LAMBDA NIL
        (SETQ THALIST (CADAR THTREE))
        (THPOPT)
        THVALUE))

(CSETQ THREMOVE
(LAMBDA (THB)
        (PROG <THB1 THWH THNF THAL THON THBS THFST THFSTP THFOO>
              <SETQ THNF 0>
              <SETQ THB1
               (COND [<ATOM THB>
                       <SETQ THBS THB>
                       <SETQ THWH (CAR (SETQ THB1 (GET THB 'THEOREM)))>
                       <CADDR THB1>]
                     [<SETQ THWH 'THASSERTION> <SETQ THBS THB>])>
              <SETQ THAL (LENGTH THB1)>
              <SETQ THFST T>
         THP1 <COND [<NULL THB1>
                      <SETQ THB1 THFOO>
                      <SETQ THNF 0>
                      <SETQ THFST (SETQ THFOO NIL)>
                      <SETQ THFSTP T>
                      <GO THP1>]
                    [<NULL (SETQ THON (THREM1 (CAR THB1)))> <RETURN NIL>
                     ]
                    [<MEMBER THON '(THBQF THVRB)>
                      <SETQ THFOO (NCONC THFOO (LIST
                       (COND [<EQ THON 'THVRB> <CAR THB1>])))>
                      <SETQ THB1 (CDR THB1)>
                      <GO THP1>]>
              <SETQ THFST NIL>
              <MAPC (CDR THB1) THREM1>
              <SETQ THNF 0>
              <MAPC THFOO THREM1>
              <RETURN THON>)))

(CSETQ THREMPROP
(LAMBDA (ATO IND)
        (THPUSH THTREE (LIST 'THMUNG (LIST (LIST 'PUT (LIST 'QUOTE ATO)
         (LIST 'QUOTE IND) (LIST 'QUOTE (GET ATO IND))))))
        (REMPROP ATO IND)))

(DEFSPEC THRESTRICT
(LAMBDA THB
        (PROG <X>
              <COND [<ATOM (SETQ X (THGAL (CAR THB) THALIST))>
                      <PRINT "THRESTRICT IGNORED - CONTINUING">]
                    [<THRPLACD (CDR X) (THUNION (CDDR X) (CDR THB))>]>
              <RETURN X>)))

(DEFMAC THRETURN
(LAMBDA (X)
        (LIST 'THSUCCEED 'THPROG X)))

(CSETQ THRPLACA
(LAMBDA (X Y)
        (PROG <THML>
              <THRPLACAS X Y>
              <THPUSH THTREE (LIST 'THMUNG THML)>
              <RETURN X>)))

(CSETQ THRPLACD
(LAMBDA (X Y)
        (PROG <THML>
              <THRPLACDS X Y>
              <THPUSH THTREE (LIST 'THMUNG THML)>
              <RETURN X>)))

(CSETQ THRPLACAS
(LAMBDA (X Y)
        (THPUSH THML (LIST 'THURPLACA X (CAR X)))
        (RPLACA X Y)))

(CSETQ THRPLACDS
(LAMBDA (X Y)
        (THPUSH THML (LIST 'THURPLACD X (CDR X)))
        (RPLACD X Y)))

(DEFSPEC THSETQ
(LAMBDA THL1
        (PROG <THML THL>
              <SETQ THL THL1>
         LOOP <COND [<NULL THL>
                      <THPUSH THTREE (LIST 'THMUNG THML)>
                      <RETURN THVALUE>]
                    [<NULL (CDR THL)>
                      <PRINT THL1>
                      <THERT "ODD NUMBER OF ARGUMENTS - THSETQ">]
                    [<ATOM (CAR THL)>
                      <THPUSH THML (LIST 'SETQ (CAR THL) (LIST 'QUOTE (
                       EVAL (CAR THL))))>
                      <SET (CAR THL) (SETQ THVALUE (EVAL (CADR THL)))>]
                    [T <THRPLACAS (CDR (THSGAL (CAR THL))) (SETQ THVALUE
                        (THVAL (CADR THL) THALIST))>]>
              <SETQ THL (CDDR THL)>
              <GO LOOP>)))

(CSETQ THSGAL
(LAMBDA (X)
        (OR [ASSOC (CADR X) THALIST]
            [PROG <Y>
                  <SETQ Y (LIST (CADR X) 'THUNASSIGNED)>
                  <NCONC THALIST (LIST Y)>
                  <RETURN Y>])))

(DEFSPEC THSTATE
(LAMBDA INDS
        (PROG <THP>
              <SETQ INDS
               (OR INDS
                   '[THASSERTION THCONSE THANTE THERASING])>
              <OBLIST
               (LAMBDA (THATOM)
                       (MAPC INDS
                        (LAMBDA (THWH)
                                (AND [SETQ THP (GET THATOM THWH)]
                                     [SETQ THP (ASSOC 1 (CDR THP))]
                                     [MAPC (CDR THP)
                                      (LAMBDA (THLENBUC)
                                              (MAPC (CDDR THLENBUC)
     (LAMBDA (ASRT)
             (COND [<EQ THWH 'THASSERTION> <PRINT ASRT>]
                   [<PRINT (LIST ASRT)>]))))]))))>
              <RETURN "DONE">)))

(DEFSPEC THSUCCEED
(LAMBDA THA
        (OR [NOT THA]
            [PROG <THX>
                  <SETQ THBRANCHV THTREE>
                  <SETQ THABRANCH THALIST>
             LOOP <COND [<NULL THTREE>
                          <PRINT THA>
                          <THERT "OVERPOP - THSUCCEED">]
                        [<EQ (CAAR THTREE) 'THREMBIND>
                          <SETQ THALIST (CADAR THTREE)>
                          <THPOPT>
                          <GO LOOP>]
                        [<EQ (CAAR THTREE) (CAR THA)>
                          <THPOPT>
                          <RETURN
                           (COND [<CDR THA> <EVAL (CADR THA)>]
                                 [T 'THNOVAL])>]
                        [<AND [EQ (CAR THA) 'THTAG]
                              [EQ (CAAR THTREE) 'THPROG]
                              [SETQ THX (MEMBER (CADR THA) (CADDDAR
                               THTREE))]>
                          <RPLACA (CDAR THTREE) (CONS NIL THX)>
                          <RETURN (THPROGT)>]
                        [T <THPOPT>
                           <GO LOOP>]>])))

(CSETQ THTAE
(LAMBDA (XX)
        (COND [<ATOM XX> NIL]
              [<EQ (CAR XX) 'THUSE>
                <MAPCAR (CDR XX)
                 (LAMBDA (X)
                         (COND [<NOT (AND [CSETQ THXX (GET X 'THEOREM)]
                                          [EQ (CAR THXX) TYPE])>
                                 <PRINT X>
                                 <THERT "BAD THEOREM - THTAE">]
                               [T <LIST 'THAPPLY X (CAR THX)>]))>]
              [<EQ (CAR XX) 'THTBF>
                <MAPCONC
                 (COND [THY1 THY]
                       [<SETQ THY1 T>
                         <SETQ THY (THMATCHLIST (CAR THX) TYPE)>])
                 (LAMBDA (Y)
                         (COND [<(EVAL (CADR XX)) Y>
                                 <LIST (LIST 'THAPPLY Y (CAR THX))>]))>]
              [T <PRINT XX>
                 <THERT "UNCLEAR RECOMMENDATION - THTAE">])))

(DEFSPEC THTAG
(LAMBDA (X)
        (AND X
             [THPUSH THTREE (LIST 'THTAG X)])))

(CSETQ THTRUE
(LAMBDA (X)
        T))

(CSETQ THTRY
(LAMBDA (X)
        (COND [<ATOM X> NIL]
              [<EQ (CAR X) 'THTBF>
                <COND [<NOT THZ1>
                        <SETQ THZ1 T>
                        <SETQ THZ (THMATCHLIST THA2 'THCONSE)>]>
                <COND [THZ <LIST (LIST 'THTBF (CADR X) THZ)>]
                      [T NIL]>]
              [<EQ (CAR X) 'THDBF>
                <COND [<NOT THY1>
                        <SETQ THY1 T>
                        <SETQ THY (THMATCHLIST THA2 'THASSERTION)>]>
                <COND [THY <LIST (LIST 'THDBF (CADR X) THY)>]
                      [T NIL]>]
              [<EQ (CAR X) 'THUSE>
                <LIST (LIST 'THTBF 'THTRUE (CDR X))>]
              [<EQ (CAR X) 'THNUM> <LIST X>]
              [T <PRINT X>
                 <THERT "UNCLEAR RECOMMENDATION - THTRY">])))

(CSETQ THTRY1
(LAMBDA NIL
        (PROG <THX THY THZ THW THEOREM>
              <SETQ THZ (CAR THTREE)>
              <SETQ THY (CDDR THZ)>
              <RPLACD THY (SUB1 (CDR THY))>
       NXTREC <COND [<OR [NULL (CAR THY)]
                         [ZEROP (CDR THY)]> <RETURN NIL>]>
              <SETQ THX (CAAR THY)>
              <COND [<EQ (SETQ THW (CAR THX)) 'THNUM> <GO THNUM>]
                    [<EQ THW 'THDBF> <GO THDBF>]
                    [<EQ THW 'THTBF> <GO THTBF>]
                    [T <PRINT THW>
                       <THERT "UNCLEAR RECOMMENDATION - THTRY1">]>
        THNUM <RPLACD THY (CADR THX)>
              <RPLACA THY (CDAR THY)>
              <GO NXTREC>
        THDBF <SETQ THOLIST THALIST>
              <COND [<NULL (CADDR THX)>
                      <RPLACA THY (CDAR THY)>
                      <GO NXTREC>]
                    [<PROG1 (AND [(EVAL (CADR THX)) (SETQ THW (CAADDR
                                  THX))]
                                 [THMATCH1 (CADR THZ) (CAR THW)]) (
                       RPLACA (CDDR THX) (CDADDR THX))> <RETURN THW>]
                    [T <GO THDBF>]>
        THTBF <COND [<NULL (CADDR THX)>
                      <RPLACA THY (CDAR THY)>
                      <GO NXTREC>]
                    [<NOT (AND [SETQ THW (GET (SETQ THEOREM (CAADDR THX)
                                ) 'THEOREM)]
                               [EQ (CAR THW) 'THCONSE])>
                      <PRINT THEOREM>
                      <THERT "BAD THEOREM - THTRY1">]
                    [<PROG1 (AND [(EVAL (CADR THX)) (CAADDR THX)]
                                 [THAPPLY1 THEOREM THW (CADR THZ)]) (
                       RPLACA (CDDR THX) (CDADDR THX))> <RETURN T>]
                    [T <GO THTBF>]>)))

(CSETQ THUNDOF
(LAMBDA NIL
        (COND [<NULL (CADDAR THTREE)> <THPOPT>]
              [T <CSETQ THXX (CDDAR THTREE)>
                 <SETQ THALIST (CAADR THXX)>
                 <RPLACA (CDR THXX) (CDADR THXX)>
                 <SETQ THTREE (CAAR THXX)>
                 <RPLACA THXX (CDAR THXX)>])
        NIL))

(CSETQ THUNDOT
(LAMBDA NIL
        (THPOPT)
        T))

(CSETQ THUNION
(LAMBDA (L1 L2)
        (MAPC L1
         (LAMBDA (THX)
                 (COND [<MEMBER THX L2>]
                       [T <SETQ L2 (CONS THX L2)>])))
        L2))

(CSETQ THUNIQUE
(LAMBDA THA
        (SETQ THA (CONS 'THUNIQUE THA))
        (PROG <X>
              <SETQ X THALIST>
           LP <COND [<NULL X>
                      <THPUSH THALIST THA>
                      <RETURN T>]
                    [<EQ (CAAR X) 'THUNIQUE>
                      <COND [<EQUAL (CAR X) THA> <RETURN NIL>]>]>
              <SETQ X (CDR X)>
              <GO LP>)))

(DEFSPEC THURPLACA
(LAMBDA (X L)
        (RPLACA X L)))

(DEFSPEC THURPLACD
(LAMBDA (X L)
        (RPLACD X L)))

(DEFSPEC THV
(LAMBDA (X)
        (THV1 X)))

(CSETQ THV1
(LAMBDA (X)
        (CSETQ THXX X)
        (COND [<EQ (SETQ X (CADR
                 (OR [ASSOC X THALIST]
                     [DO <PRINT THXX>
                         <THERT "THUNBOUND - THV1">]))) 'THUNASSIGNED>
                <PRINT THXX>
                <THERT "THUNASSIGNED - THV1">]
              [T X])))

(CSETQ THVAL
(LAMBDA (THEXP THALIST)
        (PROG <THTREE THVALUE THBRANCHV THOLIST THABRANCH THE>
              <SETQ THVALUE 'THNOVAL>
           GO <SETQ THE THEXP>
              <SETQ THEXP NIL>
              <AND THSTEP
                   [THBREAK "THSTEP:"]>
              <ATTEMPT [SETQ THVALUE (EVAL THE)]
                       [0 <CSETQ THINF T>
                          <GO FAIL>]>
          GO1 <AND THSTEPD
                   [THBREAK "THSTEPD:"]>
              <COND [THINF <GO FAIL>]
                    [THMESSAGEV <GO MFAIL>]
                    [THEXP <GO GO>]
                    [THVALUE <GO SUCCEED>]
                    [T <GO FAIL>]>
      SUCCEED <AND THSTEPT
                   [THBREAK "THSTEPT:"]>
              <COND [<NULL THBRANCHV>
                      <SETQ THBRANCHV THTREE>
                      <SETQ THABRANCH THALIST>]>
              <COND [<NULL THTREE> <RETURN THVALUE>]
                    [<SETQ THEXP (GET (CAAR THTREE) 'THSUCCEED)>
                      <GO GO2>]
                    [T <ATTEMPT [THERT "BAD SUCCEED - THVAL"]
                                [0 <GO FAIL>]>]>
        MFAIL <COND [<EQ (CAR THMESSAGEV) THTREE>
                      <SETQ THEXP (CADR THMESSAGEV)>
                      <CSETQ THMESSAGEV NIL>
                      <GO GO>]>
         FAIL <AND THSTEPF
                   [THBREAK "THSTEPF:"]>
              <COND [<NULL THTREE> <RETURN NIL>]
                    [<SETQ THEXP (GET (CAAR THTREE) 'THFAIL)> <GO GO2>]
                    [T <ATTEMPT [THERT "BAD FAIL - THVAL"]
                                [0 <GO FAIL>]>]>
          GO2 <SETQ THVALUE ((PROG1 THEXP (SETQ THEXP NIL)))>
              <GO GO1>)))

(CSETQ THVAR
(LAMBDA (X)
        (COND [<ATOM X> NIL]
              [T <MEMBER (CAR X) '(THV THNV)>])))

(CSETQ THVARS2
(LAMBDA (X)
        (PROG <A>
            L <AND [ATOM X]
                   [RETURN X]>
              <AND [EQ (CAR X) 'THEV]
                   [DO <SETQ X (THVAL (CADR X) THALIST)>
                       <GO L>]>
              <OR [THVAR X]
                  [RETURN X]>
              <SETQ A (THGAL X THALIST)>
              <RETURN
               (COND [<EQ (CADR A) 'THUNASSIGNED> X]
                     [<AND THY
                           [EQ (CAR X) 'THNV]>
                       <THRPLACA (CDR A) 'THUNASSIGNED>
                       X]
                     [T <CADR A>])>)))

(CSETQ THVARSUBST
(LAMBDA (THX THY)
        (COND [<EQ (CAR THX) 'THEV>
                <SETQ THX (THVAL (CADR THX) THALIST)>]
              [<THVAR THX> <SETQ THX (EVAL THX)>])
        (COND [<ATOM THX> THX]
              [T <MAPCAR THX THVARS2>])))

(DEFMAC THVDO
(LAMBDA L
        (LIST 'THPROG NIL (LIST 'THDO (STACK L)) '(THFINALIZE THPROG))))

(DEFSPEC THVSETQ
(LAMBDA THA
        (PROG <A>
              <SETQ A THA>
         LOOP <COND [<NULL A> <RETURN THVALUE>]
                    [<NULL (CDR A)>
                      <PRINT THA>
                      <THERT "ODD NUMBER OF ARGUMENTS - THVSETQ">]
                    [<ATOM (CAR A)>
                      <SET (CAR A) (SETQ THVALUE (EVAL (CADR A)))>]
                    [T <SETQ THVALUE (CAR (RPLACA (CDR (THSGAL (CAR A)))
                        (THVAL (CADR A) THALIST)))>]>
              <SETQ A (CDDR A)>
              <GO LOOP>)))

(PUT 'THTAG 'THFAIL THPOPTV)
(PUT 'THGOAL 'THFAIL THGOALF)
(PUT 'THFAIL? 'THFAIL THFAIL?F)
(PUT 'THAMONG 'THFAIL THAMONGF)
(PUT 'THFIND 'THFAIL THFINDF)
(PUT 'THAND 'THFAIL THANDF)
(PUT 'THPROG 'THFAIL THPROGF)
(PUT 'THMUNG 'THFAIL THMUNGF)
(PUT 'THASSERT 'THFAIL THASSERTF)
(PUT 'THERASE 'THFAIL THERASEF)
(PUT 'THCOND 'THFAIL THCONDF)
(PUT 'THOR 'THFAIL THORF)
(PUT 'THDO 'THFAIL THDOB)
(PUT 'THUNDO 'THFAIL THUNDOF)
(PUT 'THMESSAGE 'THFAIL THMESSAGEF)
(PUT 'THREMBIND 'THFAIL THREMBINDF)
(PUT 'THEOREM 'THFAIL THPOPTV)
(PUT 'THTAG 'THSUCCEED THPOPTV)
(PUT 'THGOAL 'THSUCCEED THGOALT)
(PUT 'THFAIL? 'THSUCCEED THPOPTV)
(PUT 'THFIND 'THSUCCEED THFINDT)
(PUT 'THAND 'THSUCCEED THANDT)
(PUT 'THPROG 'THSUCCEED THPROGT)
(PUT 'THMUNG 'THSUCCEED THPOPTV)
(PUT 'THASSERT 'THSUCCEED THASSERTT)
(PUT 'THERASE 'THSUCCEED THERASET)
(PUT 'THCOND 'THSUCCEED THCONDT)
(PUT 'THOR 'THSUCCEED THPOPTV)
(PUT 'THDO 'THSUCCEED THDOB)
(PUT 'THUNDO 'THSUCCEED THUNDOT)
(PUT 'THMESSAGE 'THSUCCEED THPOPTV)
(PUT 'THREMBIND 'THSUCCEED THREMBINDT)
(PUT 'THEOREM 'THSUCCEED THPOPTV)

(CSETQ THBKPT
(LAMBDA L
        (AND THTRACEV
             [THTRACES 'THBKPT L])
        THVALUE))

(CSETQ THBREAK
(LAMBDA L
        (PROG <VALUE>
              <TERPRI>
              <PRINTL (STACK L)>
         LOOP <CLEARBUFF>
              <COND [<EQ (SETQ VALUE (READ)) T> <RETURN T>]
                    [T <SETQ VALUE (EVAL VALUE)>
                       <PRIN1 "-->">
                       <PRINT VALUE>]>
              <GO LOOP>)))

(CSETQ THSEL
(LAMBDA (THF)
        (PROG <THX>
              <RETURN
               (COND [<AND [SETQ THX (ASSOC THL THTRACEV)]
                           [SETQ THX (THF THX)]> <THVAL THX THALIST>]
                     [T NIL])>)))

(CSETQ THTABPRIN1
(LAMBDA (X FLG UPDOWN)
        (SPACES THINDENT)
        (AND FLG
             [CSETQ THINDENT (PLUS THINDENT 2)])
        (PRIN1 UPDOWN)
        (PRIN1 X)
        (PRIN1 " ")))

(DEFSPEC THTRACE
(LAMBDA L
        (MAPC L THTRACE1)
        T))

(CSETQ THTRACE1
(LAMBDA (X)
        (PROG <Y>
              <SETQ X
               (COND [<ATOM X> <LIST X T NIL>]
                     [<CDDR X> X]
                     [<NULL (CDR X)>
                       <PRINT X>
                       <PRINT "BAD FORMAT">
                       <RETURN NIL>]
                     [T <LIST (CAR X) (CADR X) NIL>])>
              <COND [<GET (CAR X) 'THEOREM>
                      <COND [<SETQ Y (ASSOC 'THEOREM THTRACEV)>
                              <RPLACD Y '((THSEL CADR) (THSEL CADDR))>]
                            [T <CSETQ THTRACEV (CONS '(THEOREM (THSEL
                                CADR) (THSEL CADDR)) THTRACEV)>]>]>
              <COND [<SETQ Y (ASSOC (CAR X) THTRACEV)>
                      <RPLACD Y (CDR X)>]
                    [T <CSETQ THTRACEV (CONS X THTRACEV)>]>
              <RETURN NIL>)))

(CSETQ THTRACES
(LAMBDA (THF THL)
        (PROG <THY THZ THB>
              <AND [SETQ THY (ASSOC THF THTRACEV)]
                   [OR [SETQ THB (THVAL (CADDR THY) THALIST)]
                       [THVAL (CADR THY) THALIST]]
                   [SETQ THZ (GET THF 'THTRACE)]
                   [THZ THL THB]
                   THB
                   [THBREAK "THBREAK:"]>
              <RETURN NIL>)))

(DEFSPEC THUNTRACE
(LAMBDA THL
        (DO <COND [THL <CSETQ THTRACEV (MAPCONC THTRACEV
                        (LAMBDA (X)
                                (COND [<MEMBER (CAR X) THL>
                                        <PRINT X>
                                        NIL]
                                      [T <LIST X>])))>]
                  [T <MAPC THTRACEV PRINT>
                     <CSETQ THTRACEV NIL>]>
            T)))

(PUT 'THTRACES 'THFAIL
(LAMBDA NIL
        (CSETQ THINDENT (CADDAR THTREE))
        (THTABPRIN1 (CADAR THTREE) NIL "<")
        (PRINT "FAILED")
        (MAPC (CDDDAR THTREE) EVAL)
        (THPOPT)
        NIL))

(PUT 'THTRACES 'THSUCCEED
(LAMBDA NIL
        (CSETQ THINDENT (CADDAR THTREE))
        (THTABPRIN1 (CADAR THTREE) NIL "<")
        (PRIN1 "SUCCEEDED")
        (MAPC (CDDDAR THTREE) EVAL)
        (THPOPT)
        THVALUE))

(PUT 'THASSERT 'THTRACE
(LAMBDA (X B)
        (THPUSH THTREE (LIST 'THTRACES (GENSYM 'A) THINDENT '(TERPRI)
         (COND [B '<THBREAK "THBREAK:">]
               [T NIL])))
        (THTABPRIN1 "ASSERTING" T ">")
        (AND PSEUDO
             [PRIN1 "(THPSEUDO) "])
        (PRIN1 (CADAR THTREE))
        (PRIN1 ": ")
        (PRINT X)))

(PUT 'THGOAL 'THTRACE
(LAMBDA (X B)
        (THPUSH THTREE (LIST 'THTRACES (GENSYM 'G) THINDENT '
         (AND THVALUE
              [PRINTL ":" THVALUE]) '(TERPRI)
         (COND [B '<THBREAK "THBREAK:">]
               [T NIL])))
        (THTABPRIN1 "GOAL" T ">")
        (PRIN1 (CADAR THTREE))
        (PRIN1 ": ")
        (PRINT X)))

(PUT 'THERASE 'THTRACE
(LAMBDA (X B)
        (THPUSH THTREE (LIST 'THTRACES (GENSYM 'E) THINDENT '(TERPRI)
         (COND [B '<THBREAK "THBREAK:">]
               [T NIL])))
        (THTABPRIN1 "ERASING" T ">")
        (AND PSEUDO
             [PRIN1 "(THPSEUDO) "])
        (PRIN1 (CADAR THTREE))
        (PRIN1 ": ")
        (PRINT X)))

(PUT 'THEOREM 'THTRACE
(LAMBDA (X B)
        (THPUSH THTREE (LIST 'THTRACES X THINDENT '
         (AND THVALUE
              [PRINTL ":" THVALUE]) '(TERPRI)
         (COND [B '<THBREAK "THBREAK:">]
               [T NIL])))
        (THTABPRIN1 (CAR (GET X 'THEOREM)) T ">")
        (PRIN1 X)
        (PRIN1 ": ")
        (PRINT DAT)))

(PUT 'THBKPT 'THTRACE
(LAMBDA (X B)
        (THPUSH THTREE (LIST 'THTRACES (GENSYM 'B) THINDENT '(TERPRI)
         (COND [B '<THBREAK "THBREAK:">]
               [T NIL])))
        (THTABPRIN1 "BKPT" NIL ">")
        (PRIN1 (CADAR THTREE))
        (PRIN1 ": ")
        (SETQ THBRANCHV THTREE)
        (SETQ THABRANCH THALIST)
        (THPOPT)
        (PRINTL (STACK X))))

(DEFSPEC THEDIT
(LAMBDA (A)
        (PROG <V>
              <RETURN
               (COND [<SETQ V (GET A 'THEOREM)>
                       <PUT A 'THEOREM (EDIT1 V)>]
                     [T "CAN'T THEDIT"])>)))

(CSETQ THPRETTYP
(LAMBDA (PP-L . PP-FIL)
        (PUT 'THV 'PP-MAC "$?")
        (PUT 'THNV 'PP-MAC "$=")
        (SETQ PP-L (PRETTYP (MAPCAR PP-L
         (LAMBDA (PP-A)
                 (COND [<NOT (ATOM PP-A)> PP-A]
                       [<GET PP-A 'THEOREM> <LIST 'THEOREM PP-A>]
                       [T PP-A]))) (STACK PP-FIL)))
        (REMPROP 'THV 'PP-MAC)
        (REMPROP 'THNV 'PP-MAC)
        PP-L))

(PUT 'THCONSE 'PP-PP '(T T PP-PROG))
(PUT 'THANTE 'PP-PP '(T T PP-PROG))
(PUT 'THERASING 'PP-PP '(T T PP-PROG))
(PUT 'THCOND 'PP-PP '(T T PP-COND))
(PUT 'THPROG 'PP-PP '(T T PP-PROG))
(PUT 'THDO 'PP-PP '("<" ">" T))
(PUT 'THAND 'PP-PP '("[" "]" T))
(PUT 'THOR 'PP-PP '("[" "]" T))
(PUT 'THMESSAGE 'PP-PP '(T T PP-PROG))

(CSETQ PLNRDUMP '(";" MAP2C MAPCONC PRINTL PROG1 SPACES
         PLNR PLNRREAD THADD THAMONG THAMONGF THAND THANDF THANDT THANTE
         THAPPLY THAPPLY1 THASS1 THASSERT THASSERTLIST THASSERTF
         THASSERTT THASVAL THBAP THBI1 THBIND THBRANCH THBRANCHUN
         THCHECK THCOND THCONDF THCONDT THCONSE THDATA THDEF THDO THDOB
         THDO1 THDUMP THERASE THERASEF THERASET THERASING THERT THEV
         THFAIL THFAIL? THFAIL?F THFINALIZE THFIND THFINDF THFINDT
         THFLUSH THGAL THGENSYM THGO THGOAL THGOALF THGOALT THIP THMATCH
         THMATCH1 THMATCH2 THMATCHLIST THMESSAGE THMESSAGEF THMUNGF
         THNOFAIL THNOHASH THNOT THNV THOR THORF THOR2 THPOPT THPOPTV
         THPROG THPROGA THPROGF THPROGT THPURE THPUSH THPUT THPUTPROP
         THREM1 THREMBINDF THREMBINDT THREMOVE THREMPROP THRESTRICT
         THRETURN THRPLACA THRPLACD THRPLACAS THRPLACDS THSETQ THSGAL
         THSTATE THSUCCEED THTAE THTAG THTRUE THTRY THTRY1 THUNDOF
         THUNDOT THUNION THUNIQUE THURPLACA THURPLACD THV THV1 THVAL
         THVAR THVARS2 THVARSUBST THVDO THVSETQ (THFAIL THTAG THGOAL
         THFAIL? THAMONG THFIND THAND THPROG THMUNG THASSERT THERASE
         THCOND THOR THDO THUNDO THMESSAGE THREMBIND THEOREM) (THSUCCEED
         THTAG THGOAL THFAIL? THFIND THAND THPROG THMUNG THASSERT
         THERASE THCOND THOR THDO THUNDO THMESSAGE THREMBIND THEOREM)
         THBKPT THBREAK THSEL THTABPRIN1 THTRACE THTRACE1 THTRACES
         THUNTRACE (THFAIL THTRACES) (THSUCCEED THTRACES) (THTRACE
         THASSERT THGOAL THERASE THEOREM THBKPT) THEDIT THPRETTYP (PP-PP
         THCONSE THANTE THERASING THCOND THPROG THDO THAND THOR
         THMESSAGE) PLNRDUMP))

"PLNR LOADED"