"Copyright (c) 2015, Mark Tarver

All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright
   notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
   notice, this list of conditions and the following disclaimer in the
   documentation and/or other materials provided with the distribution.
3. The name of Mark Tarver may not be used to endorse or promote products
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY Mark Tarver ''AS IS'' AND ANY
EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL Mark Tarver BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."

(defun shen.datatype-error (V1370) (cond ((and (cons? V1370) (and (cons? (tl V1370)) (= () (tl (tl V1370))))) (simple-error (cn "datatype syntax error here:

 " (shen.app (shen.next-50 50 (hd V1370)) "
" shen.a)))) (true (shen.f_error shen.datatype-error))))

(defun shen.<datatype-rules> (V1371) (let YaccParse (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V1371) (if (not (= (fail) Parse_shen.<datatype-rule>)) (let Parse_shen.<datatype-rules> (shen.<datatype-rules> Parse_shen.<datatype-rule>) (if (not (= (fail) Parse_shen.<datatype-rules>)) (shen.pair (hd Parse_shen.<datatype-rules>) (cons (shen.hdtl Parse_shen.<datatype-rule>) (shen.hdtl Parse_shen.<datatype-rules>))) (fail))) (fail))) (if (= YaccParse (fail)) (let Parse_<e> (<e> V1371) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)))

(defun shen.<datatype-rule> (V1372) (let YaccParse (let Parse_shen.<side-conditions> (shen.<side-conditions> V1372) (if (not (= (fail) Parse_shen.<side-conditions>)) (let Parse_shen.<premises> (shen.<premises> Parse_shen.<side-conditions>) (if (not (= (fail) Parse_shen.<premises>)) (let Parse_shen.<singleunderline> (shen.<singleunderline> Parse_shen.<premises>) (if (not (= (fail) Parse_shen.<singleunderline>)) (let Parse_shen.<conclusion> (shen.<conclusion> Parse_shen.<singleunderline>) (if (not (= (fail) Parse_shen.<conclusion>)) (shen.pair (hd Parse_shen.<conclusion>) (shen.sequent shen.single (cons (shen.hdtl Parse_shen.<side-conditions>) (cons (shen.hdtl Parse_shen.<premises>) (cons (shen.hdtl Parse_shen.<conclusion>) ()))))) (fail))) (fail))) (fail))) (fail))) (if (= YaccParse (fail)) (let Parse_shen.<side-conditions> (shen.<side-conditions> V1372) (if (not (= (fail) Parse_shen.<side-conditions>)) (let Parse_shen.<premises> (shen.<premises> Parse_shen.<side-conditions>) (if (not (= (fail) Parse_shen.<premises>)) (let Parse_shen.<doubleunderline> (shen.<doubleunderline> Parse_shen.<premises>) (if (not (= (fail) Parse_shen.<doubleunderline>)) (let Parse_shen.<conclusion> (shen.<conclusion> Parse_shen.<doubleunderline>) (if (not (= (fail) Parse_shen.<conclusion>)) (shen.pair (hd Parse_shen.<conclusion>) (shen.sequent shen.double (cons (shen.hdtl Parse_shen.<side-conditions>) (cons (shen.hdtl Parse_shen.<premises>) (cons (shen.hdtl Parse_shen.<conclusion>) ()))))) (fail))) (fail))) (fail))) (fail))) YaccParse)))

(defun shen.<side-conditions> (V1373) (let YaccParse (let Parse_shen.<side-condition> (shen.<side-condition> V1373) (if (not (= (fail) Parse_shen.<side-condition>)) (let Parse_shen.<side-conditions> (shen.<side-conditions> Parse_shen.<side-condition>) (if (not (= (fail) Parse_shen.<side-conditions>)) (shen.pair (hd Parse_shen.<side-conditions>) (cons (shen.hdtl Parse_shen.<side-condition>) (shen.hdtl Parse_shen.<side-conditions>))) (fail))) (fail))) (if (= YaccParse (fail)) (let Parse_<e> (<e> V1373) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)))

(defun shen.<side-condition> (V1374) (let YaccParse (if (and (cons? (hd V1374)) (= if (hd (hd V1374)))) (let Parse_shen.<expr> (shen.<expr> (shen.pair (tl (hd V1374)) (shen.hdtl V1374))) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (cons if (cons (shen.hdtl Parse_shen.<expr>) ()))) (fail))) (fail)) (if (= YaccParse (fail)) (if (and (cons? (hd V1374)) (= let (hd (hd V1374)))) (let Parse_shen.<variable?> (shen.<variable?> (shen.pair (tl (hd V1374)) (shen.hdtl V1374))) (if (not (= (fail) Parse_shen.<variable?>)) (let Parse_shen.<expr> (shen.<expr> Parse_shen.<variable?>) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (cons let (cons (shen.hdtl Parse_shen.<variable?>) (cons (shen.hdtl Parse_shen.<expr>) ())))) (fail))) (fail))) (fail)) YaccParse)))

(defun shen.<variable?> (V1375) (if (cons? (hd V1375)) (let Parse_X (hd (hd V1375)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1375)) (shen.hdtl V1375))) Parse_X) (fail))) (fail)))

(defun shen.<expr> (V1376) (if (cons? (hd V1376)) (let Parse_X (hd (hd V1376)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1376)) (shen.hdtl V1376))) (shen.remove-bar Parse_X)) (fail))) (fail)))

(defun shen.remove-bar (V1377) (cond ((and (cons? V1377) (and (cons? (tl V1377)) (and (cons? (tl (tl V1377))) (and (= () (tl (tl (tl V1377)))) (= (hd (tl V1377)) bar!))))) (cons (hd V1377) (hd (tl (tl V1377))))) ((cons? V1377) (cons (shen.remove-bar (hd V1377)) (shen.remove-bar (tl V1377)))) (true V1377)))

(defun shen.<premises> (V1378) (let YaccParse (let Parse_shen.<premise> (shen.<premise> V1378) (if (not (= (fail) Parse_shen.<premise>)) (let Parse_shen.<semicolon-symbol> (shen.<semicolon-symbol> Parse_shen.<premise>) (if (not (= (fail) Parse_shen.<semicolon-symbol>)) (let Parse_shen.<premises> (shen.<premises> Parse_shen.<semicolon-symbol>) (if (not (= (fail) Parse_shen.<premises>)) (shen.pair (hd Parse_shen.<premises>) (cons (shen.hdtl Parse_shen.<premise>) (shen.hdtl Parse_shen.<premises>))) (fail))) (fail))) (fail))) (if (= YaccParse (fail)) (let Parse_<e> (<e> V1378) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)))

(defun shen.<semicolon-symbol> (V1379) (if (cons? (hd V1379)) (let Parse_X (hd (hd V1379)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1379)) (shen.hdtl V1379))) shen.skip) (fail))) (fail)))

(defun shen.<premise> (V1380) (let YaccParse (if (and (cons? (hd V1380)) (= ! (hd (hd V1380)))) (shen.pair (hd (shen.pair (tl (hd V1380)) (shen.hdtl V1380))) !) (fail)) (if (= YaccParse (fail)) (let YaccParse (let Parse_shen.<formulae> (shen.<formulae> V1380) (if (not (= (fail) Parse_shen.<formulae>)) (if (and (cons? (hd Parse_shen.<formulae>)) (= >> (hd (hd Parse_shen.<formulae>)))) (let Parse_shen.<formula> (shen.<formula> (shen.pair (tl (hd Parse_shen.<formulae>)) (shen.hdtl Parse_shen.<formulae>))) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (shen.sequent (shen.hdtl Parse_shen.<formulae>) (shen.hdtl Parse_shen.<formula>))) (fail))) (fail)) (fail))) (if (= YaccParse (fail)) (let Parse_shen.<formula> (shen.<formula> V1380) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (shen.sequent () (shen.hdtl Parse_shen.<formula>))) (fail))) YaccParse)) YaccParse)))

(defun shen.<conclusion> (V1381) (let YaccParse (let Parse_shen.<formulae> (shen.<formulae> V1381) (if (not (= (fail) Parse_shen.<formulae>)) (if (and (cons? (hd Parse_shen.<formulae>)) (= >> (hd (hd Parse_shen.<formulae>)))) (let Parse_shen.<formula> (shen.<formula> (shen.pair (tl (hd Parse_shen.<formulae>)) (shen.hdtl Parse_shen.<formulae>))) (if (not (= (fail) Parse_shen.<formula>)) (let Parse_shen.<semicolon-symbol> (shen.<semicolon-symbol> Parse_shen.<formula>) (if (not (= (fail) Parse_shen.<semicolon-symbol>)) (shen.pair (hd Parse_shen.<semicolon-symbol>) (shen.sequent (shen.hdtl Parse_shen.<formulae>) (shen.hdtl Parse_shen.<formula>))) (fail))) (fail))) (fail)) (fail))) (if (= YaccParse (fail)) (let Parse_shen.<formula> (shen.<formula> V1381) (if (not (= (fail) Parse_shen.<formula>)) (let Parse_shen.<semicolon-symbol> (shen.<semicolon-symbol> Parse_shen.<formula>) (if (not (= (fail) Parse_shen.<semicolon-symbol>)) (shen.pair (hd Parse_shen.<semicolon-symbol>) (shen.sequent () (shen.hdtl Parse_shen.<formula>))) (fail))) (fail))) YaccParse)))

(defun shen.sequent (V1382 V1383) (@p V1382 V1383))

(defun shen.<formulae> (V1384) (let YaccParse (let Parse_shen.<formula> (shen.<formula> V1384) (if (not (= (fail) Parse_shen.<formula>)) (let Parse_shen.<comma-symbol> (shen.<comma-symbol> Parse_shen.<formula>) (if (not (= (fail) Parse_shen.<comma-symbol>)) (let Parse_shen.<formulae> (shen.<formulae> Parse_shen.<comma-symbol>) (if (not (= (fail) Parse_shen.<formulae>)) (shen.pair (hd Parse_shen.<formulae>) (cons (shen.hdtl Parse_shen.<formula>) (shen.hdtl Parse_shen.<formulae>))) (fail))) (fail))) (fail))) (if (= YaccParse (fail)) (let YaccParse (let Parse_shen.<formula> (shen.<formula> V1384) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (cons (shen.hdtl Parse_shen.<formula>) ())) (fail))) (if (= YaccParse (fail)) (let Parse_<e> (<e> V1384) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)) YaccParse)))

(defun shen.<comma-symbol> (V1385) (if (cons? (hd V1385)) (let Parse_X (hd (hd V1385)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1385)) (shen.hdtl V1385))) shen.skip) (fail))) (fail)))

(defun shen.<formula> (V1386) (let YaccParse (let Parse_shen.<expr> (shen.<expr> V1386) (if (not (= (fail) Parse_shen.<expr>)) (if (and (cons? (hd Parse_shen.<expr>)) (= : (hd (hd Parse_shen.<expr>)))) (let Parse_shen.<type> (shen.<type> (shen.pair (tl (hd Parse_shen.<expr>)) (shen.hdtl Parse_shen.<expr>))) (if (not (= (fail) Parse_shen.<type>)) (shen.pair (hd Parse_shen.<type>) (cons (shen.curry (shen.hdtl Parse_shen.<expr>)) (cons : (cons (shen.demodulate (shen.hdtl Parse_shen.<type>)) ())))) (fail))) (fail)) (fail))) (if (= YaccParse (fail)) (let Parse_shen.<expr> (shen.<expr> V1386) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.hdtl Parse_shen.<expr>)) (fail))) YaccParse)))

(defun shen.<type> (V1387) (let Parse_shen.<expr> (shen.<expr> V1387) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.curry-type (shen.hdtl Parse_shen.<expr>))) (fail))))

(defun shen.<doubleunderline> (V1388) (if (cons? (hd V1388)) (let Parse_X (hd (hd V1388)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1388)) (shen.hdtl V1388))) Parse_X) (fail))) (fail)))

(defun shen.<singleunderline> (V1389) (if (cons? (hd V1389)) (let Parse_X (hd (hd V1389)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1389)) (shen.hdtl V1389))) Parse_X) (fail))) (fail)))

(defun shen.singleunderline? (V1390) (and (symbol? V1390) (shen.sh? (str V1390))))

(defun shen.sh? (V1391) (cond ((= "_" V1391) true) (true (and (= (pos V1391 0) "_") (shen.sh? (tlstr V1391))))))

(defun shen.doubleunderline? (V1392) (and (symbol? V1392) (shen.dh? (str V1392))))

(defun shen.dh? (V1393) (cond ((= "=" V1393) true) (true (and (= (pos V1393 0) "=") (shen.dh? (tlstr V1393))))))

(defun shen.process-datatype (V1394 V1395) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1394 V1395))))

(defun shen.remember-datatype (V1400) (cond ((cons? V1400) (do (set shen.*datatypes* (adjoin (hd V1400) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1400) (value shen.*alldatatypes*))) (hd V1400)))) (true (shen.f_error shen.remember-datatype))))

(defun shen.rules->horn-clauses (V1403 V1404) (cond ((= () V1404) ()) ((and (cons? V1404) (and (tuple? (hd V1404)) (= shen.single (fst (hd V1404))))) (cons (shen.rule->horn-clause V1403 (snd (hd V1404))) (shen.rules->horn-clauses V1403 (tl V1404)))) ((and (cons? V1404) (and (tuple? (hd V1404)) (= shen.double (fst (hd V1404))))) (shen.rules->horn-clauses V1403 (append (shen.double->singles (snd (hd V1404))) (tl V1404)))) (true (shen.f_error shen.rules->horn-clauses))))

(defun shen.double->singles (V1405) (cons (shen.right-rule V1405) (cons (shen.left-rule V1405) ())))

(defun shen.right-rule (V1406) (@p shen.single V1406))

(defun shen.left-rule (V1407) (cond ((and (cons? V1407) (and (cons? (tl V1407)) (and (cons? (tl (tl V1407))) (and (tuple? (hd (tl (tl V1407)))) (and (= () (fst (hd (tl (tl V1407))))) (= () (tl (tl (tl V1407))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1407)))) ()) Q) (let NewPremises (cons (@p (map (lambda V1359 (shen.right->left V1359)) (hd (tl V1407))) Q) ()) (@p shen.single (cons (hd V1407) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.f_error shen.left-rule))))

(defun shen.right->left (V1412) (cond ((and (tuple? V1412) (= () (fst V1412))) (snd V1412)) (true (simple-error "syntax error with ==========
"))))

(defun shen.rule->horn-clause (V1413 V1414) (cond ((and (cons? V1414) (and (cons? (tl V1414)) (and (cons? (tl (tl V1414))) (and (tuple? (hd (tl (tl V1414)))) (= () (tl (tl (tl V1414)))))))) (cons (shen.rule->horn-clause-head V1413 (snd (hd (tl (tl V1414))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1414) (hd (tl V1414)) (fst (hd (tl (tl V1414))))) ())))) (true (shen.f_error shen.rule->horn-clause))))

(defun shen.rule->horn-clause-head (V1415 V1416) (cons V1415 (cons (shen.mode-ify V1416) (cons Context_1957 ()))))

(defun shen.mode-ify (V1417) (cond ((and (cons? V1417) (and (cons? (tl V1417)) (and (= : (hd (tl V1417))) (and (cons? (tl (tl V1417))) (= () (tl (tl (tl V1417)))))))) (cons mode (cons (cons (hd V1417) (cons : (cons (cons mode (cons (hd (tl (tl V1417))) (cons + ()))) ()))) (cons - ())))) (true V1417)))

(defun shen.rule->horn-clause-body (V1418 V1419 V1420) (let Variables (map (lambda V1360 (shen.extract_vars V1360)) V1420) (let Predicates (map (lambda X (gensym shen.cl)) V1420) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1420 Variables) (let SideLiterals (shen.construct-side-literals V1418) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1420))) V1419) (append SearchLiterals (append SideLiterals PremissLiterals)))))))))

(defun shen.construct-search-literals (V1425 V1426 V1427 V1428) (cond ((and (= () V1425) (= () V1426)) ()) (true (shen.csl-help V1425 V1426 V1427 V1428))))

(defun shen.csl-help (V1431 V1432 V1433 V1434) (cond ((and (= () V1431) (= () V1432)) (cons (cons bind (cons ContextOut_1957 (cons V1433 ()))) ())) ((and (cons? V1431) (cons? V1432)) (cons (cons (hd V1431) (cons V1433 (cons V1434 (hd V1432)))) (shen.csl-help (tl V1431) (tl V1432) V1434 (gensym Context)))) (true (shen.f_error shen.csl-help))))

(defun shen.construct-search-clauses (V1435 V1436 V1437) (cond ((and (= () V1435) (and (= () V1436) (= () V1437))) shen.skip) ((and (cons? V1435) (and (cons? V1436) (cons? V1437))) (do (shen.construct-search-clause (hd V1435) (hd V1436) (hd V1437)) (shen.construct-search-clauses (tl V1435) (tl V1436) (tl V1437)))) (true (shen.f_error shen.construct-search-clauses))))

(defun shen.construct-search-clause (V1438 V1439 V1440) (shen.s-prolog (cons (shen.construct-base-search-clause V1438 V1439 V1440) (cons (shen.construct-recursive-search-clause V1438 V1439 V1440) ()))))

(defun shen.construct-base-search-clause (V1441 V1442 V1443) (cons (cons V1441 (cons (cons (shen.mode-ify V1442) In_1957) (cons In_1957 V1443))) (cons :- (cons () ()))))

(defun shen.construct-recursive-search-clause (V1444 V1445 V1446) (cons (cons V1444 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1446))) (cons :- (cons (cons (cons V1444 (cons Assumptions_1957 (cons Out_1957 V1446))) ()) ()))))

(defun shen.construct-side-literals (V1451) (cond ((= () V1451) ()) ((and (cons? V1451) (and (cons? (hd V1451)) (and (= if (hd (hd V1451))) (and (cons? (tl (hd V1451))) (= () (tl (tl (hd V1451)))))))) (cons (cons when (tl (hd V1451))) (shen.construct-side-literals (tl V1451)))) ((and (cons? V1451) (and (cons? (hd V1451)) (and (= let (hd (hd V1451))) (and (cons? (tl (hd V1451))) (and (cons? (tl (tl (hd V1451)))) (= () (tl (tl (tl (hd V1451)))))))))) (cons (cons is (tl (hd V1451))) (shen.construct-side-literals (tl V1451)))) ((cons? V1451) (shen.construct-side-literals (tl V1451))) (true (shen.f_error shen.construct-side-literals))))

(defun shen.construct-premiss-literal (V1456 V1457) (cond ((tuple? V1456) (cons shen.t* (cons (shen.recursive_cons_form (snd V1456)) (cons (shen.construct-context V1457 (fst V1456)) ())))) ((= ! V1456) (cons cut (cons Throwcontrol ()))) (true (shen.f_error shen.construct-premiss-literal))))

(defun shen.construct-context (V1458 V1459) (cond ((and (= true V1458) (= () V1459)) Context_1957) ((and (= false V1458) (= () V1459)) ContextOut_1957) ((cons? V1459) (cons cons (cons (shen.recursive_cons_form (hd V1459)) (cons (shen.construct-context V1458 (tl V1459)) ())))) (true (shen.f_error shen.construct-context))))

(defun shen.recursive_cons_form (V1460) (cond ((cons? V1460) (cons cons (cons (shen.recursive_cons_form (hd V1460)) (cons (shen.recursive_cons_form (tl V1460)) ())))) (true V1460)))

(defun preclude (V1461) (shen.preclude-h (map (lambda V1361 (shen.intern-type V1361)) V1461)))

(defun shen.preclude-h (V1462) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1462)) (value shen.*datatypes*)))

(defun include (V1463) (shen.include-h (map (lambda V1362 (shen.intern-type V1362)) V1463)))

(defun shen.include-h (V1464) (let ValidTypes (intersection V1464 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*))))

(defun preclude-all-but (V1465) (shen.preclude-h (difference (value shen.*alldatatypes*) (map (lambda V1363 (shen.intern-type V1363)) V1465))))

(defun include-all-but (V1466) (shen.include-h (difference (value shen.*alldatatypes*) (map (lambda V1364 (shen.intern-type V1364)) V1466))))

(defun shen.synonyms-help (V1471) (cond ((= () V1471) (shen.demodulation-function (value shen.*tc*) (mapcan (lambda V1365 (shen.demod-rule V1365)) (value shen.*synonyms*)))) ((and (cons? V1471) (cons? (tl V1471))) (let Vs (difference (shen.extract_vars (hd (tl V1471))) (shen.extract_vars (hd V1471))) (if (empty? Vs) (do (shen.pushnew (cons (hd V1471) (cons (hd (tl V1471)) ())) shen.*synonyms*) (shen.synonyms-help (tl (tl V1471)))) (shen.free_variable_warnings (hd (tl V1471)) Vs)))) (true (simple-error "odd number of synonyms
"))))

(defun shen.pushnew (V1472 V1473) (if (element? V1472 (value V1473)) (value V1473) (set V1473 (cons V1472 (value V1473)))))

(defun shen.demod-rule (V1474) (cond ((and (cons? V1474) (and (cons? (tl V1474)) (= () (tl (tl V1474))))) (cons (shen.rcons_form (hd V1474)) (cons -> (cons (shen.rcons_form (hd (tl V1474))) ())))) (true (shen.f_error shen.demod-rule))))

(defun shen.demodulation-function (V1475 V1476) (do (tc -) (do (eval (cons define (cons shen.demod (append V1476 (shen.default-rule))))) (do (if V1475 (tc +) shen.skip) synonyms))))

(defun shen.default-rule () (cons X (cons -> (cons X ()))))