"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 (V2519) (cond ((and (cons? V2519) (and (cons? (tl V2519)) (= () (tl (tl V2519))))) (simple-error (cn "datatype syntax error here:

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

(defun shen.<datatype-rules> (V2521) (let YaccParse (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V2521) (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> V2521) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)))

(defun shen.<datatype-rule> (V2523) (let YaccParse (let Parse_shen.<side-conditions> (shen.<side-conditions> V2523) (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> V2523) (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> (V2525) (let YaccParse (let Parse_shen.<side-condition> (shen.<side-condition> V2525) (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> V2525) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)))

(defun shen.<side-condition> (V2529) (let YaccParse (if (and (cons? (hd V2529)) (= if (shen.hdhd V2529))) (let NewStream2526 (shen.pair (shen.tlhd V2529) (shen.hdtl V2529)) (let Parse_shen.<expr> (shen.<expr> NewStream2526) (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 V2529)) (= let (shen.hdhd V2529))) (let NewStream2527 (shen.pair (shen.tlhd V2529) (shen.hdtl V2529)) (let Parse_shen.<variable?> (shen.<variable?> NewStream2527) (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?> (V2531) (if (cons? (hd V2531)) (let Parse_X (shen.hdhd V2531) (if (variable? Parse_X) (shen.pair (hd (shen.pair (shen.tlhd V2531) (shen.hdtl V2531))) Parse_X) (fail))) (fail)))

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

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

(defun shen.<premises> (V2537) (let YaccParse (let Parse_shen.<premise> (shen.<premise> V2537) (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> V2537) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)))

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

(defun shen.<premise> (V2543) (let YaccParse (if (and (cons? (hd V2543)) (= ! (shen.hdhd V2543))) (let NewStream2540 (shen.pair (shen.tlhd V2543) (shen.hdtl V2543)) (shen.pair (hd NewStream2540) !)) (fail)) (if (= YaccParse (fail)) (let YaccParse (let Parse_shen.<formulae> (shen.<formulae> V2543) (if (not (= (fail) Parse_shen.<formulae>)) (if (and (cons? (hd Parse_shen.<formulae>)) (= >> (shen.hdhd Parse_shen.<formulae>))) (let NewStream2541 (shen.pair (shen.tlhd Parse_shen.<formulae>) (shen.hdtl Parse_shen.<formulae>)) (let Parse_shen.<formula> (shen.<formula> NewStream2541) (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> V2543) (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> (V2546) (let YaccParse (let Parse_shen.<formulae> (shen.<formulae> V2546) (if (not (= (fail) Parse_shen.<formulae>)) (if (and (cons? (hd Parse_shen.<formulae>)) (= >> (shen.hdhd Parse_shen.<formulae>))) (let NewStream2544 (shen.pair (shen.tlhd Parse_shen.<formulae>) (shen.hdtl Parse_shen.<formulae>)) (let Parse_shen.<formula> (shen.<formula> NewStream2544) (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> V2546) (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 (V2549 V2550) (@p V2549 V2550))

(defun shen.<formulae> (V2552) (let YaccParse (let Parse_shen.<formula> (shen.<formula> V2552) (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> V2552) (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> V2552) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)) YaccParse)))

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

(defun shen.<formula> (V2557) (let YaccParse (let Parse_shen.<expr> (shen.<expr> V2557) (if (not (= (fail) Parse_shen.<expr>)) (if (and (cons? (hd Parse_shen.<expr>)) (= : (shen.hdhd Parse_shen.<expr>))) (let NewStream2555 (shen.pair (shen.tlhd Parse_shen.<expr>) (shen.hdtl Parse_shen.<expr>)) (let Parse_shen.<type> (shen.<type> NewStream2555) (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> V2557) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.hdtl Parse_shen.<expr>)) (fail))) YaccParse)))

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

(defun shen.<doubleunderline> (V2561) (if (cons? (hd V2561)) (let Parse_X (shen.hdhd V2561) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (shen.tlhd V2561) (shen.hdtl V2561))) Parse_X) (fail))) (fail)))

(defun shen.<singleunderline> (V2563) (if (cons? (hd V2563)) (let Parse_X (shen.hdhd V2563) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (shen.tlhd V2563) (shen.hdtl V2563))) Parse_X) (fail))) (fail)))

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

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

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

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

(defun shen.process-datatype (V2574 V2575) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V2574 V2575))))

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

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

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

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

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

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

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

(defun shen.rule->horn-clause-head (V2606 V2607) (cons V2606 (cons (shen.mode-ify V2607) (cons Context_1957 ()))))

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

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

(defun shen.construct-search-literals (V2624 V2625 V2626 V2627) (cond ((and (= () V2624) (= () V2625)) ()) (true (shen.csl-help V2624 V2625 V2626 V2627))))

(defun shen.csl-help (V2634 V2635 V2636 V2637) (cond ((and (= () V2634) (= () V2635)) (cons (cons bind (cons ContextOut_1957 (cons V2636 ()))) ())) ((and (cons? V2634) (cons? V2635)) (cons (cons (hd V2634) (cons V2636 (cons V2637 (hd V2635)))) (shen.csl-help (tl V2634) (tl V2635) V2637 (gensym Context)))) (true (shen.f_error shen.csl-help))))

(defun shen.construct-search-clauses (V2641 V2642 V2643) (cond ((and (= () V2641) (and (= () V2642) (= () V2643))) shen.skip) ((and (cons? V2641) (and (cons? V2642) (cons? V2643))) (do (shen.construct-search-clause (hd V2641) (hd V2642) (hd V2643)) (shen.construct-search-clauses (tl V2641) (tl V2642) (tl V2643)))) (true (shen.f_error shen.construct-search-clauses))))

(defun shen.construct-search-clause (V2647 V2648 V2649) (shen.s-prolog (cons (shen.construct-base-search-clause V2647 V2648 V2649) (cons (shen.construct-recursive-search-clause V2647 V2648 V2649) ()))))

(defun shen.construct-base-search-clause (V2653 V2654 V2655) (cons (cons V2653 (cons (cons (shen.mode-ify V2654) In_1957) (cons In_1957 V2655))) (cons :- (cons () ()))))

(defun shen.construct-recursive-search-clause (V2659 V2660 V2661) (cons (cons V2659 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V2661))) (cons :- (cons (cons (cons V2659 (cons Assumptions_1957 (cons Out_1957 V2661))) ()) ()))))

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

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

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

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

(defun preclude (V2683) (shen.preclude-h (map (lambda X (shen.intern-type X)) V2683)))

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

(defun include (V2687) (shen.include-h (map (lambda X (shen.intern-type X)) V2687)))

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

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

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

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

(defun shen.pushnew (V2702 V2703) (if (element? V2702 (value V2703)) (value V2703) (set V2703 (cons V2702 (value V2703)))))

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

(defun shen.lambda-of-defun (V2711) (cond ((and (cons? V2711) (and (= defun (hd V2711)) (and (cons? (tl V2711)) (and (cons? (tl (tl V2711))) (and (cons? (hd (tl (tl V2711)))) (and (= () (tl (hd (tl (tl V2711))))) (and (cons? (tl (tl (tl V2711)))) (= () (tl (tl (tl (tl V2711)))))))))))) (eval (cons /. (cons (hd (hd (tl (tl V2711)))) (tl (tl (tl V2711))))))) (true (shen.f_error shen.lambda-of-defun))))

(defun shen.update-demodulation-function (V2714 V2715) (do (tc -) (do (set shen.*demodulation-function* (shen.lambda-of-defun (shen.elim-def (cons define (cons shen.demod (append V2715 (shen.default-rule))))))) (do (if V2714 (tc +) shen.skip) synonyms))))

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