shen/release/k_lambda/t-star.kl in shen-ruby-0.9.0 vs shen/release/k_lambda/t-star.kl in shen-ruby-0.10.0

@@ -45,130 +45,95 @@
 *										                                                                    *
 * For an explication of this license see www.shenlanguage.org/license.htm which         *
 * explains this license in full.                                                        *
 *				 						                                                                    *
 *****************************************************************************************
-"(defun shen.typecheck (V2882 V2883) (let Curry (shen.curry V2882) (let ProcessN (shen.start-new-prolog-process) (let Type (shen.insert-prolog-variables (shen.demodulate (shen.curry-type V2883)) ProcessN) (let Continuation (freeze (return Type ProcessN shen.void)) (shen.t* (cons Curry (cons : (cons Type ()))) () ProcessN Continuation))))))
+"(defun shen.typecheck (V2790 V2791) (let Curry (shen.curry V2790) (let ProcessN (shen.start-new-prolog-process) (let Type (shen.insert-prolog-variables (shen.demodulate (shen.curry-type V2791)) ProcessN) (let Continuation (freeze (return Type ProcessN shen.void)) (shen.t* (cons Curry (cons : (cons Type ()))) () ProcessN Continuation))))))
 
-(defun shen.curry (V2884) (cond ((and (cons? V2884) (shen.special? (hd V2884))) (cons (hd V2884) (map (lambda X2877 (shen.curry X2877)) (tl V2884)))) ((and (cons? V2884) (and (cons? (tl V2884)) (shen.extraspecial? (hd V2884)))) V2884) ((and (cons? V2884) (and (= type (hd V2884)) (and (cons? (tl V2884)) (and (cons? (tl (tl V2884))) (= () (tl (tl (tl V2884)))))))) (cons type (cons (shen.curry (hd (tl V2884))) (tl (tl V2884))))) ((and (cons? V2884) (and (cons? (tl V2884)) (cons? (tl (tl V2884))))) (shen.curry (cons (cons (hd V2884) (cons (hd (tl V2884)) ())) (tl (tl V2884))))) ((and (cons? V2884) (and (cons? (tl V2884)) (= () (tl (tl V2884))))) (cons (shen.curry (hd V2884)) (cons (shen.curry (hd (tl V2884))) ()))) (true V2884)))
+(defun shen.curry (V2792) (cond ((and (cons? V2792) (shen.special? (hd V2792))) (cons (hd V2792) (map (lambda X2786 (shen.curry X2786)) (tl V2792)))) ((and (cons? V2792) (and (cons? (tl V2792)) (shen.extraspecial? (hd V2792)))) V2792) ((and (cons? V2792) (and (= type (hd V2792)) (and (cons? (tl V2792)) (and (cons? (tl (tl V2792))) (= () (tl (tl (tl V2792)))))))) (cons type (cons (shen.curry (hd (tl V2792))) (tl (tl V2792))))) ((and (cons? V2792) (and (cons? (tl V2792)) (cons? (tl (tl V2792))))) (shen.curry (cons (cons (hd V2792) (cons (hd (tl V2792)) ())) (tl (tl V2792))))) ((and (cons? V2792) (and (cons? (tl V2792)) (= () (tl (tl V2792))))) (cons (shen.curry (hd V2792)) (cons (shen.curry (hd (tl V2792))) ()))) (true V2792)))
 
-(defun shen.special? (V2885) (element? V2885 (value shen.*special*)))
+(defun shen.special? (V2793) (element? V2793 (value shen.*special*)))
 
-(defun shen.extraspecial? (V2886) (element? V2886 (value shen.*extraspecial*)))
+(defun shen.extraspecial? (V2794) (element? V2794 (value shen.*extraspecial*)))
 
-(defun shen.t* (V2887 V2888 V2889 V2890) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let Error (shen.newpv V2889) (do (shen.incinfs) (fwhen (shen.maxinfexceeded?) V2889 (freeze (bind Error (shen.errormaxinfs) V2889 V2890))))) (if (= Case false) (let Case (let V2871 (shen.lazyderef V2887 V2889) (if (= fail V2871) (do (shen.incinfs) (cut Throwcontrol V2889 (freeze (shen.prolog-failure V2889 V2890)))) false)) (if (= Case false) (let Case (let V2872 (shen.lazyderef V2887 V2889) (if (cons? V2872) (let X (hd V2872) (let V2873 (shen.lazyderef (tl V2872) V2889) (if (cons? V2873) (let V2874 (shen.lazyderef (hd V2873) V2889) (if (= : V2874) (let V2875 (shen.lazyderef (tl V2873) V2889) (if (cons? V2875) (let A (hd V2875) (let V2876 (shen.lazyderef (tl V2875) V2889) (if (= () V2876) (do (shen.incinfs) (fwhen (shen.type-theory-enabled?) V2889 (freeze (cut Throwcontrol V2889 (freeze (shen.th* X A V2888 V2889 V2890)))))) false))) false)) false)) false))) false)) (if (= Case false) (let Datatypes (shen.newpv V2889) (do (shen.incinfs) (shen.show V2887 V2888 V2889 (freeze (bind Datatypes (value shen.*datatypes*) V2889 (freeze (shen.udefs* V2887 V2888 Datatypes V2889 V2890))))))) Case)) Case)) Case)))))
+(defun shen.t* (V2795 V2796 V2797 V2798) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let Error (shen.newpv V2797) (do (shen.incinfs) (fwhen (shen.maxinfexceeded?) V2797 (freeze (bind Error (shen.errormaxinfs) V2797 V2798))))) (if (= Case false) (let Case (let V2780 (shen.lazyderef V2795 V2797) (if (= fail V2780) (do (shen.incinfs) (cut Throwcontrol V2797 (freeze (shen.prolog-failure V2797 V2798)))) false)) (if (= Case false) (let Case (let V2781 (shen.lazyderef V2795 V2797) (if (cons? V2781) (let X (hd V2781) (let V2782 (shen.lazyderef (tl V2781) V2797) (if (cons? V2782) (let V2783 (shen.lazyderef (hd V2782) V2797) (if (= : V2783) (let V2784 (shen.lazyderef (tl V2782) V2797) (if (cons? V2784) (let A (hd V2784) (let V2785 (shen.lazyderef (tl V2784) V2797) (if (= () V2785) (do (shen.incinfs) (fwhen (shen.type-theory-enabled?) V2797 (freeze (cut Throwcontrol V2797 (freeze (shen.th* X A V2796 V2797 V2798)))))) false))) false)) false)) false))) false)) (if (= Case false) (let Datatypes (shen.newpv V2797) (do (shen.incinfs) (shen.show V2795 V2796 V2797 (freeze (bind Datatypes (value shen.*datatypes*) V2797 (freeze (shen.udefs* V2795 V2796 Datatypes V2797 V2798))))))) Case)) Case)) Case)))))
 
 (defun shen.type-theory-enabled? () (value shen.*shen-type-theory-enabled?*))
 
-(defun enable-type-theory (V2895) (cond ((= + V2895) (set shen.*shen-type-theory-enabled?* true)) ((= - V2895) (set shen.*shen-type-theory-enabled?* false)) (true (simple-error "enable-type-theory expects a + or a -
+(defun enable-type-theory (V2803) (cond ((= + V2803) (set shen.*shen-type-theory-enabled?* true)) ((= - V2803) (set shen.*shen-type-theory-enabled?* false)) (true (simple-error "enable-type-theory expects a + or a -
 "))))
 
-(defun shen.prolog-failure (V2904 V2905) false)
+(defun shen.prolog-failure (V2812 V2813) false)
 
 (defun shen.maxinfexceeded? () (> (inferences) (value shen.*maxinferences*)))
 
 (defun shen.errormaxinfs () (simple-error "maximum inferences exceeded~%"))
 
-(defun shen.udefs* (V2906 V2907 V2908 V2909 V2910) (let Case (let V2867 (shen.lazyderef V2908 V2909) (if (cons? V2867) (let D (hd V2867) (do (shen.incinfs) (call (cons D (cons V2906 (cons V2907 ()))) V2909 V2910))) false)) (if (= Case false) (let V2868 (shen.lazyderef V2908 V2909) (if (cons? V2868) (let Ds (tl V2868) (do (shen.incinfs) (shen.udefs* V2906 V2907 Ds V2909 V2910))) false)) Case)))
+(defun shen.udefs* (V2814 V2815 V2816 V2817 V2818) (let Case (let V2776 (shen.lazyderef V2816 V2817) (if (cons? V2776) (let D (hd V2776) (do (shen.incinfs) (call (cons D (cons V2814 (cons V2815 ()))) V2817 V2818))) false)) (if (= Case false) (let V2777 (shen.lazyderef V2816 V2817) (if (cons? V2777) (let Ds (tl V2777) (do (shen.incinfs) (shen.udefs* V2814 V2815 Ds V2817 V2818))) false)) Case)))
 
-(defun shen.th* (V2911 V2912 V2913 V2914 V2915) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (do (shen.incinfs) (shen.show (cons V2911 (cons : (cons V2912 ()))) V2913 V2914 (freeze (fwhen false V2914 V2915)))) (if (= Case false) (let Case (let F (shen.newpv V2914) (do (shen.incinfs) (fwhen (shen.typedf? (shen.lazyderef V2911 V2914)) V2914 (freeze (bind F (shen.sigf (shen.lazyderef V2911 V2914)) V2914 (freeze (call (cons F (cons V2912 ())) V2914 V2915))))))) (if (= Case false) (let Case (do (shen.incinfs) (shen.base V2911 V2912 V2914 V2915)) (if (= Case false) (let Case (do (shen.incinfs) (shen.by_hypothesis V2911 V2912 V2913 V2914 V2915)) (if (= Case false) (let Case (let V2752 (shen.lazyderef V2911 V2914) (if (cons? V2752) (let F (hd V2752) (let V2753 (shen.lazyderef (tl V2752) V2914) (if (= () V2753) (do (shen.incinfs) (shen.th* F (cons --> (cons V2912 ())) V2913 V2914 V2915)) false))) false)) (if (= Case false) (let Case (let V2754 (shen.lazyderef V2911 V2914) (if (cons? V2754) (let F (hd V2754) (let V2755 (shen.lazyderef (tl V2754) V2914) (if (cons? V2755) (let X (hd V2755) (let V2756 (shen.lazyderef (tl V2755) V2914) (if (= () V2756) (let B (shen.newpv V2914) (do (shen.incinfs) (shen.th* F (cons B (cons --> (cons V2912 ()))) V2913 V2914 (freeze (shen.th* X B V2913 V2914 V2915))))) false))) false))) false)) (if (= Case false) (let Case (let V2757 (shen.lazyderef V2911 V2914) (if (cons? V2757) (let V2758 (shen.lazyderef (hd V2757) V2914) (if (= cons V2758) (let V2759 (shen.lazyderef (tl V2757) V2914) (if (cons? V2759) (let X (hd V2759) (let V2760 (shen.lazyderef (tl V2759) V2914) (if (cons? V2760) (let Y (hd V2760) (let V2761 (shen.lazyderef (tl V2760) V2914) (if (= () V2761) (let V2762 (shen.lazyderef V2912 V2914) (if (cons? V2762) (let V2763 (shen.lazyderef (hd V2762) V2914) (if (= list V2763) (let V2764 (shen.lazyderef (tl V2762) V2914) (if (cons? V2764) (let A (hd V2764) (let V2765 (shen.lazyderef (tl V2764) V2914) (if (= () V2765) (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons list (cons A ())) V2913 V2914 V2915)))) (if (shen.pvar? V2765) (do (shen.bindv V2765 () V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons list (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2765 V2914) Result))) false)))) (if (shen.pvar? V2764) (let A (shen.newpv V2914) (do (shen.bindv V2764 (cons A ()) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons list (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2764 V2914) Result)))) false))) (if (shen.pvar? V2763) (do (shen.bindv V2763 list V2914) (let Result (let V2766 (shen.lazyderef (tl V2762) V2914) (if (cons? V2766) (let A (hd V2766) (let V2767 (shen.lazyderef (tl V2766) V2914) (if (= () V2767) (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons list (cons A ())) V2913 V2914 V2915)))) (if (shen.pvar? V2767) (do (shen.bindv V2767 () V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons list (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2767 V2914) Result))) false)))) (if (shen.pvar? V2766) (let A (shen.newpv V2914) (do (shen.bindv V2766 (cons A ()) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons list (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2766 V2914) Result)))) false))) (do (shen.unbindv V2763 V2914) Result))) false))) (if (shen.pvar? V2762) (let A (shen.newpv V2914) (do (shen.bindv V2762 (cons list (cons A ())) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons list (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2762 V2914) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2768 (shen.lazyderef V2911 V2914) (if (cons? V2768) (let V2769 (shen.lazyderef (hd V2768) V2914) (if (= @p V2769) (let V2770 (shen.lazyderef (tl V2768) V2914) (if (cons? V2770) (let X (hd V2770) (let V2771 (shen.lazyderef (tl V2770) V2914) (if (cons? V2771) (let Y (hd V2771) (let V2772 (shen.lazyderef (tl V2771) V2914) (if (= () V2772) (let V2773 (shen.lazyderef V2912 V2914) (if (cons? V2773) (let A (hd V2773) (let V2774 (shen.lazyderef (tl V2773) V2914) (if (cons? V2774) (let V2775 (shen.lazyderef (hd V2774) V2914) (if (= * V2775) (let V2776 (shen.lazyderef (tl V2774) V2914) (if (cons? V2776) (let B (hd V2776) (let V2777 (shen.lazyderef (tl V2776) V2914) (if (= () V2777) (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y B V2913 V2914 V2915)))) (if (shen.pvar? V2777) (do (shen.bindv V2777 () V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y B V2913 V2914 V2915)))) (do (shen.unbindv V2777 V2914) Result))) false)))) (if (shen.pvar? V2776) (let B (shen.newpv V2914) (do (shen.bindv V2776 (cons B ()) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y B V2913 V2914 V2915)))) (do (shen.unbindv V2776 V2914) Result)))) false))) (if (shen.pvar? V2775) (do (shen.bindv V2775 * V2914) (let Result (let V2778 (shen.lazyderef (tl V2774) V2914) (if (cons? V2778) (let B (hd V2778) (let V2779 (shen.lazyderef (tl V2778) V2914) (if (= () V2779) (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y B V2913 V2914 V2915)))) (if (shen.pvar? V2779) (do (shen.bindv V2779 () V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y B V2913 V2914 V2915)))) (do (shen.unbindv V2779 V2914) Result))) false)))) (if (shen.pvar? V2778) (let B (shen.newpv V2914) (do (shen.bindv V2778 (cons B ()) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y B V2913 V2914 V2915)))) (do (shen.unbindv V2778 V2914) Result)))) false))) (do (shen.unbindv V2775 V2914) Result))) false))) (if (shen.pvar? V2774) (let B (shen.newpv V2914) (do (shen.bindv V2774 (cons * (cons B ())) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y B V2913 V2914 V2915)))) (do (shen.unbindv V2774 V2914) Result)))) false)))) (if (shen.pvar? V2773) (let A (shen.newpv V2914) (let B (shen.newpv V2914) (do (shen.bindv V2773 (cons A (cons * (cons B ()))) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y B V2913 V2914 V2915)))) (do (shen.unbindv V2773 V2914) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2780 (shen.lazyderef V2911 V2914) (if (cons? V2780) (let V2781 (shen.lazyderef (hd V2780) V2914) (if (= @v V2781) (let V2782 (shen.lazyderef (tl V2780) V2914) (if (cons? V2782) (let X (hd V2782) (let V2783 (shen.lazyderef (tl V2782) V2914) (if (cons? V2783) (let Y (hd V2783) (let V2784 (shen.lazyderef (tl V2783) V2914) (if (= () V2784) (let V2785 (shen.lazyderef V2912 V2914) (if (cons? V2785) (let V2786 (shen.lazyderef (hd V2785) V2914) (if (= vector V2786) (let V2787 (shen.lazyderef (tl V2785) V2914) (if (cons? V2787) (let A (hd V2787) (let V2788 (shen.lazyderef (tl V2787) V2914) (if (= () V2788) (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons vector (cons A ())) V2913 V2914 V2915)))) (if (shen.pvar? V2788) (do (shen.bindv V2788 () V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons vector (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2788 V2914) Result))) false)))) (if (shen.pvar? V2787) (let A (shen.newpv V2914) (do (shen.bindv V2787 (cons A ()) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons vector (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2787 V2914) Result)))) false))) (if (shen.pvar? V2786) (do (shen.bindv V2786 vector V2914) (let Result (let V2789 (shen.lazyderef (tl V2785) V2914) (if (cons? V2789) (let A (hd V2789) (let V2790 (shen.lazyderef (tl V2789) V2914) (if (= () V2790) (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons vector (cons A ())) V2913 V2914 V2915)))) (if (shen.pvar? V2790) (do (shen.bindv V2790 () V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons vector (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2790 V2914) Result))) false)))) (if (shen.pvar? V2789) (let A (shen.newpv V2914) (do (shen.bindv V2789 (cons A ()) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons vector (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2789 V2914) Result)))) false))) (do (shen.unbindv V2786 V2914) Result))) false))) (if (shen.pvar? V2785) (let A (shen.newpv V2914) (do (shen.bindv V2785 (cons vector (cons A ())) V2914) (let Result (do (shen.incinfs) (shen.th* X A V2913 V2914 (freeze (shen.th* Y (cons vector (cons A ())) V2913 V2914 V2915)))) (do (shen.unbindv V2785 V2914) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2791 (shen.lazyderef V2911 V2914) (if (cons? V2791) (let V2792 (shen.lazyderef (hd V2791) V2914) (if (= @s V2792) (let V2793 (shen.lazyderef (tl V2791) V2914) (if (cons? V2793) (let X (hd V2793) (let V2794 (shen.lazyderef (tl V2793) V2914) (if (cons? V2794) (let Y (hd V2794) (let V2795 (shen.lazyderef (tl V2794) V2914) (if (= () V2795) (let V2796 (shen.lazyderef V2912 V2914) (if (= string V2796) (do (shen.incinfs) (shen.th* X string V2913 V2914 (freeze (shen.th* Y string V2913 V2914 V2915)))) (if (shen.pvar? V2796) (do (shen.bindv V2796 string V2914) (let Result (do (shen.incinfs) (shen.th* X string V2913 V2914 (freeze (shen.th* Y string V2913 V2914 V2915)))) (do (shen.unbindv V2796 V2914) Result))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2797 (shen.lazyderef V2911 V2914) (if (cons? V2797) (let V2798 (shen.lazyderef (hd V2797) V2914) (if (= lambda V2798) (let V2799 (shen.lazyderef (tl V2797) V2914) (if (cons? V2799) (let X (hd V2799) (let V2800 (shen.lazyderef (tl V2799) V2914) (if (cons? V2800) (let Y (hd V2800) (let V2801 (shen.lazyderef (tl V2800) V2914) (if (= () V2801) (let V2802 (shen.lazyderef V2912 V2914) (if (cons? V2802) (let A (hd V2802) (let V2803 (shen.lazyderef (tl V2802) V2914) (if (cons? V2803) (let V2804 (shen.lazyderef (hd V2803) V2914) (if (= --> V2804) (let V2805 (shen.lazyderef (tl V2803) V2914) (if (cons? V2805) (let B (hd V2805) (let V2806 (shen.lazyderef (tl V2805) V2914) (if (= () V2806) (let Z (shen.newpv V2914) (let X&& (shen.newpv V2914) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (bind X&& (shen.placeholder) V2914 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2914) (shen.lazyderef X V2914) (shen.lazyderef Y V2914)) V2914 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2913) V2914 V2915)))))))))) (if (shen.pvar? V2806) (do (shen.bindv V2806 () V2914) (let Result (let Z (shen.newpv V2914) (let X&& (shen.newpv V2914) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (bind X&& (shen.placeholder) V2914 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2914) (shen.lazyderef X V2914) (shen.lazyderef Y V2914)) V2914 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2913) V2914 V2915)))))))))) (do (shen.unbindv V2806 V2914) Result))) false)))) (if (shen.pvar? V2805) (let B (shen.newpv V2914) (do (shen.bindv V2805 (cons B ()) V2914) (let Result (let Z (shen.newpv V2914) (let X&& (shen.newpv V2914) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (bind X&& (shen.placeholder) V2914 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2914) (shen.lazyderef X V2914) (shen.lazyderef Y V2914)) V2914 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2913) V2914 V2915)))))))))) (do (shen.unbindv V2805 V2914) Result)))) false))) (if (shen.pvar? V2804) (do (shen.bindv V2804 --> V2914) (let Result (let V2807 (shen.lazyderef (tl V2803) V2914) (if (cons? V2807) (let B (hd V2807) (let V2808 (shen.lazyderef (tl V2807) V2914) (if (= () V2808) (let Z (shen.newpv V2914) (let X&& (shen.newpv V2914) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (bind X&& (shen.placeholder) V2914 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2914) (shen.lazyderef X V2914) (shen.lazyderef Y V2914)) V2914 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2913) V2914 V2915)))))))))) (if (shen.pvar? V2808) (do (shen.bindv V2808 () V2914) (let Result (let Z (shen.newpv V2914) (let X&& (shen.newpv V2914) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (bind X&& (shen.placeholder) V2914 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2914) (shen.lazyderef X V2914) (shen.lazyderef Y V2914)) V2914 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2913) V2914 V2915)))))))))) (do (shen.unbindv V2808 V2914) Result))) false)))) (if (shen.pvar? V2807) (let B (shen.newpv V2914) (do (shen.bindv V2807 (cons B ()) V2914) (let Result (let Z (shen.newpv V2914) (let X&& (shen.newpv V2914) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (bind X&& (shen.placeholder) V2914 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2914) (shen.lazyderef X V2914) (shen.lazyderef Y V2914)) V2914 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2913) V2914 V2915)))))))))) (do (shen.unbindv V2807 V2914) Result)))) false))) (do (shen.unbindv V2804 V2914) Result))) false))) (if (shen.pvar? V2803) (let B (shen.newpv V2914) (do (shen.bindv V2803 (cons --> (cons B ())) V2914) (let Result (let Z (shen.newpv V2914) (let X&& (shen.newpv V2914) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (bind X&& (shen.placeholder) V2914 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2914) (shen.lazyderef X V2914) (shen.lazyderef Y V2914)) V2914 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2913) V2914 V2915)))))))))) (do (shen.unbindv V2803 V2914) Result)))) false)))) (if (shen.pvar? V2802) (let A (shen.newpv V2914) (let B (shen.newpv V2914) (do (shen.bindv V2802 (cons A (cons --> (cons B ()))) V2914) (let Result (let Z (shen.newpv V2914) (let X&& (shen.newpv V2914) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (bind X&& (shen.placeholder) V2914 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2914) (shen.lazyderef X V2914) (shen.lazyderef Y V2914)) V2914 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2913) V2914 V2915)))))))))) (do (shen.unbindv V2802 V2914) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2809 (shen.lazyderef V2911 V2914) (if (cons? V2809) (let V2810 (shen.lazyderef (hd V2809) V2914) (if (= let V2810) (let V2811 (shen.lazyderef (tl V2809) V2914) (if (cons? V2811) (let X (hd V2811) (let V2812 (shen.lazyderef (tl V2811) V2914) (if (cons? V2812) (let Y (hd V2812) (let V2813 (shen.lazyderef (tl V2812) V2914) (if (cons? V2813) (let Z (hd V2813) (let V2814 (shen.lazyderef (tl V2813) V2914) (if (= () V2814) (let W (shen.newpv V2914) (let X&& (shen.newpv V2914) (let B (shen.newpv V2914) (do (shen.incinfs) (shen.th* Y B V2913 V2914 (freeze (bind X&& (shen.placeholder) V2914 (freeze (bind W (shen.ebr (shen.lazyderef X&& V2914) (shen.lazyderef X V2914) (shen.lazyderef Z V2914)) V2914 (freeze (shen.th* W V2912 (cons (cons X&& (cons : (cons B ()))) V2913) V2914 V2915))))))))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2815 (shen.lazyderef V2911 V2914) (if (cons? V2815) (let V2816 (shen.lazyderef (hd V2815) V2914) (if (= open V2816) (let V2817 (shen.lazyderef (tl V2815) V2914) (if (cons? V2817) (let FileName (hd V2817) (let V2818 (shen.lazyderef (tl V2817) V2914) (if (cons? V2818) (let Direction2748 (hd V2818) (let V2819 (shen.lazyderef (tl V2818) V2914) (if (= () V2819) (let V2820 (shen.lazyderef V2912 V2914) (if (cons? V2820) (let V2821 (shen.lazyderef (hd V2820) V2914) (if (= stream V2821) (let V2822 (shen.lazyderef (tl V2820) V2914) (if (cons? V2822) (let Direction (hd V2822) (let V2823 (shen.lazyderef (tl V2822) V2914) (if (= () V2823) (do (shen.incinfs) (unify! Direction Direction2748 V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.th* FileName string V2913 V2914 V2915)))))) (if (shen.pvar? V2823) (do (shen.bindv V2823 () V2914) (let Result (do (shen.incinfs) (unify! Direction Direction2748 V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.th* FileName string V2913 V2914 V2915)))))) (do (shen.unbindv V2823 V2914) Result))) false)))) (if (shen.pvar? V2822) (let Direction (shen.newpv V2914) (do (shen.bindv V2822 (cons Direction ()) V2914) (let Result (do (shen.incinfs) (unify! Direction Direction2748 V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.th* FileName string V2913 V2914 V2915)))))) (do (shen.unbindv V2822 V2914) Result)))) false))) (if (shen.pvar? V2821) (do (shen.bindv V2821 stream V2914) (let Result (let V2824 (shen.lazyderef (tl V2820) V2914) (if (cons? V2824) (let Direction (hd V2824) (let V2825 (shen.lazyderef (tl V2824) V2914) (if (= () V2825) (do (shen.incinfs) (unify! Direction Direction2748 V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.th* FileName string V2913 V2914 V2915)))))) (if (shen.pvar? V2825) (do (shen.bindv V2825 () V2914) (let Result (do (shen.incinfs) (unify! Direction Direction2748 V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.th* FileName string V2913 V2914 V2915)))))) (do (shen.unbindv V2825 V2914) Result))) false)))) (if (shen.pvar? V2824) (let Direction (shen.newpv V2914) (do (shen.bindv V2824 (cons Direction ()) V2914) (let Result (do (shen.incinfs) (unify! Direction Direction2748 V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.th* FileName string V2913 V2914 V2915)))))) (do (shen.unbindv V2824 V2914) Result)))) false))) (do (shen.unbindv V2821 V2914) Result))) false))) (if (shen.pvar? V2820) (let Direction (shen.newpv V2914) (do (shen.bindv V2820 (cons stream (cons Direction ())) V2914) (let Result (do (shen.incinfs) (unify! Direction Direction2748 V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.th* FileName string V2913 V2914 V2915)))))) (do (shen.unbindv V2820 V2914) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2826 (shen.lazyderef V2911 V2914) (if (cons? V2826) (let V2827 (shen.lazyderef (hd V2826) V2914) (if (= type V2827) (let V2828 (shen.lazyderef (tl V2826) V2914) (if (cons? V2828) (let X (hd V2828) (let V2829 (shen.lazyderef (tl V2828) V2914) (if (cons? V2829) (let A (hd V2829) (let V2830 (shen.lazyderef (tl V2829) V2914) (if (= () V2830) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (unify A V2912 V2914 (freeze (shen.th* X A V2913 V2914 V2915)))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2831 (shen.lazyderef V2911 V2914) (if (cons? V2831) (let V2832 (shen.lazyderef (hd V2831) V2914) (if (= input+ V2832) (let V2833 (shen.lazyderef (tl V2831) V2914) (if (cons? V2833) (let A (hd V2833) (let V2834 (shen.lazyderef (tl V2833) V2914) (if (cons? V2834) (let Stream (hd V2834) (let V2835 (shen.lazyderef (tl V2834) V2914) (if (= () V2835) (let C (shen.newpv V2914) (do (shen.incinfs) (bind C (shen.demodulate (shen.lazyderef A V2914)) V2914 (freeze (unify V2912 C V2914 (freeze (shen.th* Stream (cons stream (cons in ())) V2913 V2914 V2915))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2836 (shen.lazyderef V2911 V2914) (if (cons? V2836) (let V2837 (shen.lazyderef (hd V2836) V2914) (if (= set V2837) (let V2838 (shen.lazyderef (tl V2836) V2914) (if (cons? V2838) (let Var (hd V2838) (let V2839 (shen.lazyderef (tl V2838) V2914) (if (cons? V2839) (let Val (hd V2839) (let V2840 (shen.lazyderef (tl V2839) V2914) (if (= () V2840) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (shen.th* Var symbol V2913 V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.th* (cons value (cons Var ())) V2912 V2913 V2914 (freeze (shen.th* Val V2912 V2913 V2914 V2915)))))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2841 (shen.lazyderef V2911 V2914) (if (cons? V2841) (let V2842 (shen.lazyderef (hd V2841) V2914) (if (= shen.<-sem V2842) (let V2843 (shen.lazyderef (tl V2841) V2914) (if (cons? V2843) (let F (hd V2843) (let V2844 (shen.lazyderef (tl V2843) V2914) (if (= () V2844) (let A (shen.newpv V2914) (let F&& (shen.newpv V2914) (let B (shen.newpv V2914) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (shen.th* F (cons A (cons ==> (cons B ()))) V2913 V2914 (freeze (cut Throwcontrol V2914 (freeze (bind F&& (concat && (shen.lazyderef F V2914)) V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.th* F&& V2912 (cons (cons F&& (cons : (cons B ()))) V2913) V2914 V2915))))))))))))))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2845 (shen.lazyderef V2911 V2914) (if (cons? V2845) (let V2846 (shen.lazyderef (hd V2845) V2914) (if (= fail V2846) (let V2847 (shen.lazyderef (tl V2845) V2914) (if (= () V2847) (let V2848 (shen.lazyderef V2912 V2914) (if (= symbol V2848) (do (shen.incinfs) (thaw V2915)) (if (shen.pvar? V2848) (do (shen.bindv V2848 symbol V2914) (let Result (do (shen.incinfs) (thaw V2915)) (do (shen.unbindv V2848 V2914) Result))) false))) false)) false)) false)) (if (= Case false) (let Case (let NewHyp (shen.newpv V2914) (do (shen.incinfs) (shen.t*-hyps V2913 NewHyp V2914 (freeze (shen.th* V2911 V2912 NewHyp V2914 V2915))))) (if (= Case false) (let Case (let V2849 (shen.lazyderef V2911 V2914) (if (cons? V2849) (let V2850 (shen.lazyderef (hd V2849) V2914) (if (= define V2850) (let V2851 (shen.lazyderef (tl V2849) V2914) (if (cons? V2851) (let F (hd V2851) (let X (tl V2851) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (shen.t*-def (cons define (cons F X)) V2912 V2913 V2914 V2915)))))) false)) false)) false)) (if (= Case false) (let Case (let V2852 (shen.lazyderef V2911 V2914) (if (cons? V2852) (let V2853 (shen.lazyderef (hd V2852) V2914) (if (= defcc V2853) (let V2854 (shen.lazyderef (tl V2852) V2914) (if (cons? V2854) (let F (hd V2854) (let X (tl V2854) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (shen.t*-defcc (cons defcc (cons F X)) V2912 V2913 V2914 V2915)))))) false)) false)) false)) (if (= Case false) (let Case (let V2855 (shen.lazyderef V2911 V2914) (if (cons? V2855) (let V2856 (shen.lazyderef (hd V2855) V2914) (if (= defmacro V2856) (let V2857 (shen.lazyderef V2912 V2914) (if (= unit V2857) (do (shen.incinfs) (cut Throwcontrol V2914 V2915)) (if (shen.pvar? V2857) (do (shen.bindv V2857 unit V2914) (let Result (do (shen.incinfs) (cut Throwcontrol V2914 V2915)) (do (shen.unbindv V2857 V2914) Result))) false))) false)) false)) (if (= Case false) (let Case (let V2858 (shen.lazyderef V2911 V2914) (if (cons? V2858) (let V2859 (shen.lazyderef (hd V2858) V2914) (if (= shen.process-datatype V2859) (let V2860 (shen.lazyderef V2912 V2914) (if (= symbol V2860) (do (shen.incinfs) (thaw V2915)) (if (shen.pvar? V2860) (do (shen.bindv V2860 symbol V2914) (let Result (do (shen.incinfs) (thaw V2915)) (do (shen.unbindv V2860 V2914) Result))) false))) false)) false)) (if (= Case false) (let Case (let V2861 (shen.lazyderef V2911 V2914) (if (cons? V2861) (let V2862 (shen.lazyderef (hd V2861) V2914) (if (= shen.synonyms-help V2862) (let V2863 (shen.lazyderef V2912 V2914) (if (= symbol V2863) (do (shen.incinfs) (thaw V2915)) (if (shen.pvar? V2863) (do (shen.bindv V2863 symbol V2914) (let Result (do (shen.incinfs) (thaw V2915)) (do (shen.unbindv V2863 V2914) Result))) false))) false)) false)) (if (= Case false) (let Datatypes (shen.newpv V2914) (do (shen.incinfs) (bind Datatypes (value shen.*datatypes*) V2914 (freeze (shen.udefs* (cons V2911 (cons : (cons V2912 ()))) V2913 Datatypes V2914 V2915))))) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)))))
+(defun shen.th* (V2819 V2820 V2821 V2822 V2823) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (do (shen.incinfs) (shen.show (cons V2819 (cons : (cons V2820 ()))) V2821 V2822 (freeze (fwhen false V2822 V2823)))) (if (= Case false) (let Case (let F (shen.newpv V2822) (do (shen.incinfs) (fwhen (shen.typedf? (shen.lazyderef V2819 V2822)) V2822 (freeze (bind F (shen.sigf (shen.lazyderef V2819 V2822)) V2822 (freeze (call (cons F (cons V2820 ())) V2822 V2823))))))) (if (= Case false) (let Case (do (shen.incinfs) (shen.base V2819 V2820 V2822 V2823)) (if (= Case false) (let Case (do (shen.incinfs) (shen.by_hypothesis V2819 V2820 V2821 V2822 V2823)) (if (= Case false) (let Case (let V2668 (shen.lazyderef V2819 V2822) (if (cons? V2668) (let F (hd V2668) (let V2669 (shen.lazyderef (tl V2668) V2822) (if (= () V2669) (do (shen.incinfs) (shen.th* F (cons --> (cons V2820 ())) V2821 V2822 V2823)) false))) false)) (if (= Case false) (let Case (let V2670 (shen.lazyderef V2819 V2822) (if (cons? V2670) (let F (hd V2670) (let V2671 (shen.lazyderef (tl V2670) V2822) (if (cons? V2671) (let X (hd V2671) (let V2672 (shen.lazyderef (tl V2671) V2822) (if (= () V2672) (let B (shen.newpv V2822) (do (shen.incinfs) (shen.th* F (cons B (cons --> (cons V2820 ()))) V2821 V2822 (freeze (shen.th* X B V2821 V2822 V2823))))) false))) false))) false)) (if (= Case false) (let Case (let V2673 (shen.lazyderef V2819 V2822) (if (cons? V2673) (let V2674 (shen.lazyderef (hd V2673) V2822) (if (= cons V2674) (let V2675 (shen.lazyderef (tl V2673) V2822) (if (cons? V2675) (let X (hd V2675) (let V2676 (shen.lazyderef (tl V2675) V2822) (if (cons? V2676) (let Y (hd V2676) (let V2677 (shen.lazyderef (tl V2676) V2822) (if (= () V2677) (let V2678 (shen.lazyderef V2820 V2822) (if (cons? V2678) (let V2679 (shen.lazyderef (hd V2678) V2822) (if (= list V2679) (let V2680 (shen.lazyderef (tl V2678) V2822) (if (cons? V2680) (let A (hd V2680) (let V2681 (shen.lazyderef (tl V2680) V2822) (if (= () V2681) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2681) (do (shen.bindv V2681 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2681 V2822) Result))) false)))) (if (shen.pvar? V2680) (let A (shen.newpv V2822) (do (shen.bindv V2680 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2680 V2822) Result)))) false))) (if (shen.pvar? V2679) (do (shen.bindv V2679 list V2822) (let Result (let V2682 (shen.lazyderef (tl V2678) V2822) (if (cons? V2682) (let A (hd V2682) (let V2683 (shen.lazyderef (tl V2682) V2822) (if (= () V2683) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2683) (do (shen.bindv V2683 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2683 V2822) Result))) false)))) (if (shen.pvar? V2682) (let A (shen.newpv V2822) (do (shen.bindv V2682 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2682 V2822) Result)))) false))) (do (shen.unbindv V2679 V2822) Result))) false))) (if (shen.pvar? V2678) (let A (shen.newpv V2822) (do (shen.bindv V2678 (cons list (cons A ())) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2678 V2822) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2684 (shen.lazyderef V2819 V2822) (if (cons? V2684) (let V2685 (shen.lazyderef (hd V2684) V2822) (if (= @p V2685) (let V2686 (shen.lazyderef (tl V2684) V2822) (if (cons? V2686) (let X (hd V2686) (let V2687 (shen.lazyderef (tl V2686) V2822) (if (cons? V2687) (let Y (hd V2687) (let V2688 (shen.lazyderef (tl V2687) V2822) (if (= () V2688) (let V2689 (shen.lazyderef V2820 V2822) (if (cons? V2689) (let A (hd V2689) (let V2690 (shen.lazyderef (tl V2689) V2822) (if (cons? V2690) (let V2691 (shen.lazyderef (hd V2690) V2822) (if (= * V2691) (let V2692 (shen.lazyderef (tl V2690) V2822) (if (cons? V2692) (let B (hd V2692) (let V2693 (shen.lazyderef (tl V2692) V2822) (if (= () V2693) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (if (shen.pvar? V2693) (do (shen.bindv V2693 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2693 V2822) Result))) false)))) (if (shen.pvar? V2692) (let B (shen.newpv V2822) (do (shen.bindv V2692 (cons B ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2692 V2822) Result)))) false))) (if (shen.pvar? V2691) (do (shen.bindv V2691 * V2822) (let Result (let V2694 (shen.lazyderef (tl V2690) V2822) (if (cons? V2694) (let B (hd V2694) (let V2695 (shen.lazyderef (tl V2694) V2822) (if (= () V2695) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (if (shen.pvar? V2695) (do (shen.bindv V2695 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2695 V2822) Result))) false)))) (if (shen.pvar? V2694) (let B (shen.newpv V2822) (do (shen.bindv V2694 (cons B ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2694 V2822) Result)))) false))) (do (shen.unbindv V2691 V2822) Result))) false))) (if (shen.pvar? V2690) (let B (shen.newpv V2822) (do (shen.bindv V2690 (cons * (cons B ())) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2690 V2822) Result)))) false)))) (if (shen.pvar? V2689) (let A (shen.newpv V2822) (let B (shen.newpv V2822) (do (shen.bindv V2689 (cons A (cons * (cons B ()))) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2689 V2822) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2696 (shen.lazyderef V2819 V2822) (if (cons? V2696) (let V2697 (shen.lazyderef (hd V2696) V2822) (if (= @v V2697) (let V2698 (shen.lazyderef (tl V2696) V2822) (if (cons? V2698) (let X (hd V2698) (let V2699 (shen.lazyderef (tl V2698) V2822) (if (cons? V2699) (let Y (hd V2699) (let V2700 (shen.lazyderef (tl V2699) V2822) (if (= () V2700) (let V2701 (shen.lazyderef V2820 V2822) (if (cons? V2701) (let V2702 (shen.lazyderef (hd V2701) V2822) (if (= vector V2702) (let V2703 (shen.lazyderef (tl V2701) V2822) (if (cons? V2703) (let A (hd V2703) (let V2704 (shen.lazyderef (tl V2703) V2822) (if (= () V2704) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2704) (do (shen.bindv V2704 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2704 V2822) Result))) false)))) (if (shen.pvar? V2703) (let A (shen.newpv V2822) (do (shen.bindv V2703 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2703 V2822) Result)))) false))) (if (shen.pvar? V2702) (do (shen.bindv V2702 vector V2822) (let Result (let V2705 (shen.lazyderef (tl V2701) V2822) (if (cons? V2705) (let A (hd V2705) (let V2706 (shen.lazyderef (tl V2705) V2822) (if (= () V2706) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2706) (do (shen.bindv V2706 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2706 V2822) Result))) false)))) (if (shen.pvar? V2705) (let A (shen.newpv V2822) (do (shen.bindv V2705 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2705 V2822) Result)))) false))) (do (shen.unbindv V2702 V2822) Result))) false))) (if (shen.pvar? V2701) (let A (shen.newpv V2822) (do (shen.bindv V2701 (cons vector (cons A ())) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2701 V2822) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2707 (shen.lazyderef V2819 V2822) (if (cons? V2707) (let V2708 (shen.lazyderef (hd V2707) V2822) (if (= @s V2708) (let V2709 (shen.lazyderef (tl V2707) V2822) (if (cons? V2709) (let X (hd V2709) (let V2710 (shen.lazyderef (tl V2709) V2822) (if (cons? V2710) (let Y (hd V2710) (let V2711 (shen.lazyderef (tl V2710) V2822) (if (= () V2711) (let V2712 (shen.lazyderef V2820 V2822) (if (= string V2712) (do (shen.incinfs) (shen.th* X string V2821 V2822 (freeze (shen.th* Y string V2821 V2822 V2823)))) (if (shen.pvar? V2712) (do (shen.bindv V2712 string V2822) (let Result (do (shen.incinfs) (shen.th* X string V2821 V2822 (freeze (shen.th* Y string V2821 V2822 V2823)))) (do (shen.unbindv V2712 V2822) Result))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2713 (shen.lazyderef V2819 V2822) (if (cons? V2713) (let V2714 (shen.lazyderef (hd V2713) V2822) (if (= lambda V2714) (let V2715 (shen.lazyderef (tl V2713) V2822) (if (cons? V2715) (let X (hd V2715) (let V2716 (shen.lazyderef (tl V2715) V2822) (if (cons? V2716) (let Y (hd V2716) (let V2717 (shen.lazyderef (tl V2716) V2822) (if (= () V2717) (let V2718 (shen.lazyderef V2820 V2822) (if (cons? V2718) (let A (hd V2718) (let V2719 (shen.lazyderef (tl V2718) V2822) (if (cons? V2719) (let V2720 (shen.lazyderef (hd V2719) V2822) (if (= --> V2720) (let V2721 (shen.lazyderef (tl V2719) V2822) (if (cons? V2721) (let B (hd V2721) (let V2722 (shen.lazyderef (tl V2721) V2822) (if (= () V2722) (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (if (shen.pvar? V2722) (do (shen.bindv V2722 () V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2722 V2822) Result))) false)))) (if (shen.pvar? V2721) (let B (shen.newpv V2822) (do (shen.bindv V2721 (cons B ()) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2721 V2822) Result)))) false))) (if (shen.pvar? V2720) (do (shen.bindv V2720 --> V2822) (let Result (let V2723 (shen.lazyderef (tl V2719) V2822) (if (cons? V2723) (let B (hd V2723) (let V2724 (shen.lazyderef (tl V2723) V2822) (if (= () V2724) (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (if (shen.pvar? V2724) (do (shen.bindv V2724 () V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2724 V2822) Result))) false)))) (if (shen.pvar? V2723) (let B (shen.newpv V2822) (do (shen.bindv V2723 (cons B ()) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2723 V2822) Result)))) false))) (do (shen.unbindv V2720 V2822) Result))) false))) (if (shen.pvar? V2719) (let B (shen.newpv V2822) (do (shen.bindv V2719 (cons --> (cons B ())) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2719 V2822) Result)))) false)))) (if (shen.pvar? V2718) (let A (shen.newpv V2822) (let B (shen.newpv V2822) (do (shen.bindv V2718 (cons A (cons --> (cons B ()))) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2718 V2822) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2725 (shen.lazyderef V2819 V2822) (if (cons? V2725) (let V2726 (shen.lazyderef (hd V2725) V2822) (if (= let V2726) (let V2727 (shen.lazyderef (tl V2725) V2822) (if (cons? V2727) (let X (hd V2727) (let V2728 (shen.lazyderef (tl V2727) V2822) (if (cons? V2728) (let Y (hd V2728) (let V2729 (shen.lazyderef (tl V2728) V2822) (if (cons? V2729) (let Z (hd V2729) (let V2730 (shen.lazyderef (tl V2729) V2822) (if (= () V2730) (let W (shen.newpv V2822) (let X&& (shen.newpv V2822) (let B (shen.newpv V2822) (do (shen.incinfs) (shen.th* Y B V2821 V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind W (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Z V2822)) V2822 (freeze (shen.th* W V2820 (cons (cons X&& (cons : (cons B ()))) V2821) V2822 V2823))))))))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2731 (shen.lazyderef V2819 V2822) (if (cons? V2731) (let V2732 (shen.lazyderef (hd V2731) V2822) (if (= open V2732) (let V2733 (shen.lazyderef (tl V2731) V2822) (if (cons? V2733) (let FileName (hd V2733) (let V2734 (shen.lazyderef (tl V2733) V2822) (if (cons? V2734) (let Direction2664 (hd V2734) (let V2735 (shen.lazyderef (tl V2734) V2822) (if (= () V2735) (let V2736 (shen.lazyderef V2820 V2822) (if (cons? V2736) (let V2737 (shen.lazyderef (hd V2736) V2822) (if (= stream V2737) (let V2738 (shen.lazyderef (tl V2736) V2822) (if (cons? V2738) (let Direction (hd V2738) (let V2739 (shen.lazyderef (tl V2738) V2822) (if (= () V2739) (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (if (shen.pvar? V2739) (do (shen.bindv V2739 () V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2739 V2822) Result))) false)))) (if (shen.pvar? V2738) (let Direction (shen.newpv V2822) (do (shen.bindv V2738 (cons Direction ()) V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2738 V2822) Result)))) false))) (if (shen.pvar? V2737) (do (shen.bindv V2737 stream V2822) (let Result (let V2740 (shen.lazyderef (tl V2736) V2822) (if (cons? V2740) (let Direction (hd V2740) (let V2741 (shen.lazyderef (tl V2740) V2822) (if (= () V2741) (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (if (shen.pvar? V2741) (do (shen.bindv V2741 () V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2741 V2822) Result))) false)))) (if (shen.pvar? V2740) (let Direction (shen.newpv V2822) (do (shen.bindv V2740 (cons Direction ()) V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2740 V2822) Result)))) false))) (do (shen.unbindv V2737 V2822) Result))) false))) (if (shen.pvar? V2736) (let Direction (shen.newpv V2822) (do (shen.bindv V2736 (cons stream (cons Direction ())) V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2736 V2822) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2742 (shen.lazyderef V2819 V2822) (if (cons? V2742) (let V2743 (shen.lazyderef (hd V2742) V2822) (if (= type V2743) (let V2744 (shen.lazyderef (tl V2742) V2822) (if (cons? V2744) (let X (hd V2744) (let V2745 (shen.lazyderef (tl V2744) V2822) (if (cons? V2745) (let A (hd V2745) (let V2746 (shen.lazyderef (tl V2745) V2822) (if (= () V2746) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (unify A V2820 V2822 (freeze (shen.th* X A V2821 V2822 V2823)))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2747 (shen.lazyderef V2819 V2822) (if (cons? V2747) (let V2748 (shen.lazyderef (hd V2747) V2822) (if (= input+ V2748) (let V2749 (shen.lazyderef (tl V2747) V2822) (if (cons? V2749) (let A (hd V2749) (let V2750 (shen.lazyderef (tl V2749) V2822) (if (cons? V2750) (let Stream (hd V2750) (let V2751 (shen.lazyderef (tl V2750) V2822) (if (= () V2751) (let C (shen.newpv V2822) (do (shen.incinfs) (bind C (shen.demodulate (shen.lazyderef A V2822)) V2822 (freeze (unify V2820 C V2822 (freeze (shen.th* Stream (cons stream (cons in ())) V2821 V2822 V2823))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2752 (shen.lazyderef V2819 V2822) (if (cons? V2752) (let V2753 (shen.lazyderef (hd V2752) V2822) (if (= set V2753) (let V2754 (shen.lazyderef (tl V2752) V2822) (if (cons? V2754) (let Var (hd V2754) (let V2755 (shen.lazyderef (tl V2754) V2822) (if (cons? V2755) (let Val (hd V2755) (let V2756 (shen.lazyderef (tl V2755) V2822) (if (= () V2756) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (shen.th* Var symbol V2821 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* (cons value (cons Var ())) V2820 V2821 V2822 (freeze (shen.th* Val V2820 V2821 V2822 V2823)))))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2757 (shen.lazyderef V2819 V2822) (if (cons? V2757) (let V2758 (shen.lazyderef (hd V2757) V2822) (if (= fail V2758) (let V2759 (shen.lazyderef (tl V2757) V2822) (if (= () V2759) (let V2760 (shen.lazyderef V2820 V2822) (if (= symbol V2760) (do (shen.incinfs) (thaw V2823)) (if (shen.pvar? V2760) (do (shen.bindv V2760 symbol V2822) (let Result (do (shen.incinfs) (thaw V2823)) (do (shen.unbindv V2760 V2822) Result))) false))) false)) false)) false)) (if (= Case false) (let Case (let NewHyp (shen.newpv V2822) (do (shen.incinfs) (shen.t*-hyps V2821 NewHyp V2822 (freeze (shen.th* V2819 V2820 NewHyp V2822 V2823))))) (if (= Case false) (let Case (let V2761 (shen.lazyderef V2819 V2822) (if (cons? V2761) (let V2762 (shen.lazyderef (hd V2761) V2822) (if (= define V2762) (let V2763 (shen.lazyderef (tl V2761) V2822) (if (cons? V2763) (let F (hd V2763) (let X (tl V2763) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (shen.t*-def (cons define (cons F X)) V2820 V2821 V2822 V2823)))))) false)) false)) false)) (if (= Case false) (let Case (let V2764 (shen.lazyderef V2819 V2822) (if (cons? V2764) (let V2765 (shen.lazyderef (hd V2764) V2822) (if (= defmacro V2765) (let V2766 (shen.lazyderef V2820 V2822) (if (= unit V2766) (do (shen.incinfs) (cut Throwcontrol V2822 V2823)) (if (shen.pvar? V2766) (do (shen.bindv V2766 unit V2822) (let Result (do (shen.incinfs) (cut Throwcontrol V2822 V2823)) (do (shen.unbindv V2766 V2822) Result))) false))) false)) false)) (if (= Case false) (let Case (let V2767 (shen.lazyderef V2819 V2822) (if (cons? V2767) (let V2768 (shen.lazyderef (hd V2767) V2822) (if (= shen.process-datatype V2768) (let V2769 (shen.lazyderef V2820 V2822) (if (= symbol V2769) (do (shen.incinfs) (thaw V2823)) (if (shen.pvar? V2769) (do (shen.bindv V2769 symbol V2822) (let Result (do (shen.incinfs) (thaw V2823)) (do (shen.unbindv V2769 V2822) Result))) false))) false)) false)) (if (= Case false) (let Case (let V2770 (shen.lazyderef V2819 V2822) (if (cons? V2770) (let V2771 (shen.lazyderef (hd V2770) V2822) (if (= shen.synonyms-help V2771) (let V2772 (shen.lazyderef V2820 V2822) (if (= symbol V2772) (do (shen.incinfs) (thaw V2823)) (if (shen.pvar? V2772) (do (shen.bindv V2772 symbol V2822) (let Result (do (shen.incinfs) (thaw V2823)) (do (shen.unbindv V2772 V2822) Result))) false))) false)) false)) (if (= Case false) (let Datatypes (shen.newpv V2822) (do (shen.incinfs) (bind Datatypes (value shen.*datatypes*) V2822 (freeze (shen.udefs* (cons V2819 (cons : (cons V2820 ()))) V2821 Datatypes V2822 V2823))))) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)))))
 
-(defun shen.t*-hyps (V2916 V2917 V2918 V2919) (let Case (let V2663 (shen.lazyderef V2916 V2918) (if (cons? V2663) (let V2664 (shen.lazyderef (hd V2663) V2918) (if (cons? V2664) (let V2665 (shen.lazyderef (hd V2664) V2918) (if (cons? V2665) (let V2666 (shen.lazyderef (hd V2665) V2918) (if (= cons V2666) (let V2667 (shen.lazyderef (tl V2665) V2918) (if (cons? V2667) (let X (hd V2667) (let V2668 (shen.lazyderef (tl V2667) V2918) (if (cons? V2668) (let Y (hd V2668) (let V2669 (shen.lazyderef (tl V2668) V2918) (if (= () V2669) (let V2670 (shen.lazyderef (tl V2664) V2918) (if (cons? V2670) (let V2671 (shen.lazyderef (hd V2670) V2918) (if (= : V2671) (let V2672 (shen.lazyderef (tl V2670) V2918) (if (cons? V2672) (let V2673 (shen.lazyderef (hd V2672) V2918) (if (cons? V2673) (let V2674 (shen.lazyderef (hd V2673) V2918) (if (= list V2674) (let V2675 (shen.lazyderef (tl V2673) V2918) (if (cons? V2675) (let A (hd V2675) (let V2676 (shen.lazyderef (tl V2675) V2918) (if (= () V2676) (let V2677 (shen.lazyderef (tl V2672) V2918) (if (= () V2677) (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2677) (do (shen.bindv V2677 () V2918) (let Result (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2677 V2918) Result))) false))) (if (shen.pvar? V2676) (do (shen.bindv V2676 () V2918) (let Result (let V2678 (shen.lazyderef (tl V2672) V2918) (if (= () V2678) (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2678) (do (shen.bindv V2678 () V2918) (let Result (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2678 V2918) Result))) false))) (do (shen.unbindv V2676 V2918) Result))) false)))) (if (shen.pvar? V2675) (let A (shen.newpv V2918) (do (shen.bindv V2675 (cons A ()) V2918) (let Result (let V2679 (shen.lazyderef (tl V2672) V2918) (if (= () V2679) (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2679) (do (shen.bindv V2679 () V2918) (let Result (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2679 V2918) Result))) false))) (do (shen.unbindv V2675 V2918) Result)))) false))) (if (shen.pvar? V2674) (do (shen.bindv V2674 list V2918) (let Result (let V2680 (shen.lazyderef (tl V2673) V2918) (if (cons? V2680) (let A (hd V2680) (let V2681 (shen.lazyderef (tl V2680) V2918) (if (= () V2681) (let V2682 (shen.lazyderef (tl V2672) V2918) (if (= () V2682) (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2682) (do (shen.bindv V2682 () V2918) (let Result (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2682 V2918) Result))) false))) (if (shen.pvar? V2681) (do (shen.bindv V2681 () V2918) (let Result (let V2683 (shen.lazyderef (tl V2672) V2918) (if (= () V2683) (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2683) (do (shen.bindv V2683 () V2918) (let Result (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2683 V2918) Result))) false))) (do (shen.unbindv V2681 V2918) Result))) false)))) (if (shen.pvar? V2680) (let A (shen.newpv V2918) (do (shen.bindv V2680 (cons A ()) V2918) (let Result (let V2684 (shen.lazyderef (tl V2672) V2918) (if (= () V2684) (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2684) (do (shen.bindv V2684 () V2918) (let Result (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2684 V2918) Result))) false))) (do (shen.unbindv V2680 V2918) Result)))) false))) (do (shen.unbindv V2674 V2918) Result))) false))) (if (shen.pvar? V2673) (let A (shen.newpv V2918) (do (shen.bindv V2673 (cons list (cons A ())) V2918) (let Result (let V2685 (shen.lazyderef (tl V2672) V2918) (if (= () V2685) (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2685) (do (shen.bindv V2685 () V2918) (let Result (let Hyp (tl V2663) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons list (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2685 V2918) Result))) false))) (do (shen.unbindv V2673 V2918) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2686 (shen.lazyderef V2916 V2918) (if (cons? V2686) (let V2687 (shen.lazyderef (hd V2686) V2918) (if (cons? V2687) (let V2688 (shen.lazyderef (hd V2687) V2918) (if (cons? V2688) (let V2689 (shen.lazyderef (hd V2688) V2918) (if (= @p V2689) (let V2690 (shen.lazyderef (tl V2688) V2918) (if (cons? V2690) (let X (hd V2690) (let V2691 (shen.lazyderef (tl V2690) V2918) (if (cons? V2691) (let Y (hd V2691) (let V2692 (shen.lazyderef (tl V2691) V2918) (if (= () V2692) (let V2693 (shen.lazyderef (tl V2687) V2918) (if (cons? V2693) (let V2694 (shen.lazyderef (hd V2693) V2918) (if (= : V2694) (let V2695 (shen.lazyderef (tl V2693) V2918) (if (cons? V2695) (let V2696 (shen.lazyderef (hd V2695) V2918) (if (cons? V2696) (let A (hd V2696) (let V2697 (shen.lazyderef (tl V2696) V2918) (if (cons? V2697) (let V2698 (shen.lazyderef (hd V2697) V2918) (if (= * V2698) (let V2699 (shen.lazyderef (tl V2697) V2918) (if (cons? V2699) (let B (hd V2699) (let V2700 (shen.lazyderef (tl V2699) V2918) (if (= () V2700) (let V2701 (shen.lazyderef (tl V2695) V2918) (if (= () V2701) (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2701) (do (shen.bindv V2701 () V2918) (let Result (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2701 V2918) Result))) false))) (if (shen.pvar? V2700) (do (shen.bindv V2700 () V2918) (let Result (let V2702 (shen.lazyderef (tl V2695) V2918) (if (= () V2702) (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2702) (do (shen.bindv V2702 () V2918) (let Result (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2702 V2918) Result))) false))) (do (shen.unbindv V2700 V2918) Result))) false)))) (if (shen.pvar? V2699) (let B (shen.newpv V2918) (do (shen.bindv V2699 (cons B ()) V2918) (let Result (let V2703 (shen.lazyderef (tl V2695) V2918) (if (= () V2703) (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2703) (do (shen.bindv V2703 () V2918) (let Result (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2703 V2918) Result))) false))) (do (shen.unbindv V2699 V2918) Result)))) false))) (if (shen.pvar? V2698) (do (shen.bindv V2698 * V2918) (let Result (let V2704 (shen.lazyderef (tl V2697) V2918) (if (cons? V2704) (let B (hd V2704) (let V2705 (shen.lazyderef (tl V2704) V2918) (if (= () V2705) (let V2706 (shen.lazyderef (tl V2695) V2918) (if (= () V2706) (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2706) (do (shen.bindv V2706 () V2918) (let Result (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2706 V2918) Result))) false))) (if (shen.pvar? V2705) (do (shen.bindv V2705 () V2918) (let Result (let V2707 (shen.lazyderef (tl V2695) V2918) (if (= () V2707) (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2707) (do (shen.bindv V2707 () V2918) (let Result (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2707 V2918) Result))) false))) (do (shen.unbindv V2705 V2918) Result))) false)))) (if (shen.pvar? V2704) (let B (shen.newpv V2918) (do (shen.bindv V2704 (cons B ()) V2918) (let Result (let V2708 (shen.lazyderef (tl V2695) V2918) (if (= () V2708) (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2708) (do (shen.bindv V2708 () V2918) (let Result (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2708 V2918) Result))) false))) (do (shen.unbindv V2704 V2918) Result)))) false))) (do (shen.unbindv V2698 V2918) Result))) false))) (if (shen.pvar? V2697) (let B (shen.newpv V2918) (do (shen.bindv V2697 (cons * (cons B ())) V2918) (let Result (let V2709 (shen.lazyderef (tl V2695) V2918) (if (= () V2709) (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2709) (do (shen.bindv V2709 () V2918) (let Result (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2709 V2918) Result))) false))) (do (shen.unbindv V2697 V2918) Result)))) false)))) (if (shen.pvar? V2696) (let A (shen.newpv V2918) (let B (shen.newpv V2918) (do (shen.bindv V2696 (cons A (cons * (cons B ()))) V2918) (let Result (let V2710 (shen.lazyderef (tl V2695) V2918) (if (= () V2710) (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2710) (do (shen.bindv V2710 () V2918) (let Result (let Hyp (tl V2686) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (shen.lazyderef B V2918) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2710 V2918) Result))) false))) (do (shen.unbindv V2696 V2918) Result))))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2711 (shen.lazyderef V2916 V2918) (if (cons? V2711) (let V2712 (shen.lazyderef (hd V2711) V2918) (if (cons? V2712) (let V2713 (shen.lazyderef (hd V2712) V2918) (if (cons? V2713) (let V2714 (shen.lazyderef (hd V2713) V2918) (if (= @v V2714) (let V2715 (shen.lazyderef (tl V2713) V2918) (if (cons? V2715) (let X (hd V2715) (let V2716 (shen.lazyderef (tl V2715) V2918) (if (cons? V2716) (let Y (hd V2716) (let V2717 (shen.lazyderef (tl V2716) V2918) (if (= () V2717) (let V2718 (shen.lazyderef (tl V2712) V2918) (if (cons? V2718) (let V2719 (shen.lazyderef (hd V2718) V2918) (if (= : V2719) (let V2720 (shen.lazyderef (tl V2718) V2918) (if (cons? V2720) (let V2721 (shen.lazyderef (hd V2720) V2918) (if (cons? V2721) (let V2722 (shen.lazyderef (hd V2721) V2918) (if (= vector V2722) (let V2723 (shen.lazyderef (tl V2721) V2918) (if (cons? V2723) (let A (hd V2723) (let V2724 (shen.lazyderef (tl V2723) V2918) (if (= () V2724) (let V2725 (shen.lazyderef (tl V2720) V2918) (if (= () V2725) (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2725) (do (shen.bindv V2725 () V2918) (let Result (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2725 V2918) Result))) false))) (if (shen.pvar? V2724) (do (shen.bindv V2724 () V2918) (let Result (let V2726 (shen.lazyderef (tl V2720) V2918) (if (= () V2726) (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2726) (do (shen.bindv V2726 () V2918) (let Result (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2726 V2918) Result))) false))) (do (shen.unbindv V2724 V2918) Result))) false)))) (if (shen.pvar? V2723) (let A (shen.newpv V2918) (do (shen.bindv V2723 (cons A ()) V2918) (let Result (let V2727 (shen.lazyderef (tl V2720) V2918) (if (= () V2727) (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2727) (do (shen.bindv V2727 () V2918) (let Result (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2727 V2918) Result))) false))) (do (shen.unbindv V2723 V2918) Result)))) false))) (if (shen.pvar? V2722) (do (shen.bindv V2722 vector V2918) (let Result (let V2728 (shen.lazyderef (tl V2721) V2918) (if (cons? V2728) (let A (hd V2728) (let V2729 (shen.lazyderef (tl V2728) V2918) (if (= () V2729) (let V2730 (shen.lazyderef (tl V2720) V2918) (if (= () V2730) (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2730) (do (shen.bindv V2730 () V2918) (let Result (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2730 V2918) Result))) false))) (if (shen.pvar? V2729) (do (shen.bindv V2729 () V2918) (let Result (let V2731 (shen.lazyderef (tl V2720) V2918) (if (= () V2731) (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2731) (do (shen.bindv V2731 () V2918) (let Result (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2731 V2918) Result))) false))) (do (shen.unbindv V2729 V2918) Result))) false)))) (if (shen.pvar? V2728) (let A (shen.newpv V2918) (do (shen.bindv V2728 (cons A ()) V2918) (let Result (let V2732 (shen.lazyderef (tl V2720) V2918) (if (= () V2732) (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2732) (do (shen.bindv V2732 () V2918) (let Result (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2732 V2918) Result))) false))) (do (shen.unbindv V2728 V2918) Result)))) false))) (do (shen.unbindv V2722 V2918) Result))) false))) (if (shen.pvar? V2721) (let A (shen.newpv V2918) (do (shen.bindv V2721 (cons vector (cons A ())) V2918) (let Result (let V2733 (shen.lazyderef (tl V2720) V2918) (if (= () V2733) (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2733) (do (shen.bindv V2733 () V2918) (let Result (let Hyp (tl V2711) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons (shen.lazyderef A V2918) ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons (cons vector (cons (shen.lazyderef A V2918) ())) ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2733 V2918) Result))) false))) (do (shen.unbindv V2721 V2918) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2734 (shen.lazyderef V2916 V2918) (if (cons? V2734) (let V2735 (shen.lazyderef (hd V2734) V2918) (if (cons? V2735) (let V2736 (shen.lazyderef (hd V2735) V2918) (if (cons? V2736) (let V2737 (shen.lazyderef (hd V2736) V2918) (if (= @s V2737) (let V2738 (shen.lazyderef (tl V2736) V2918) (if (cons? V2738) (let X (hd V2738) (let V2739 (shen.lazyderef (tl V2738) V2918) (if (cons? V2739) (let Y (hd V2739) (let V2740 (shen.lazyderef (tl V2739) V2918) (if (= () V2740) (let V2741 (shen.lazyderef (tl V2735) V2918) (if (cons? V2741) (let V2742 (shen.lazyderef (hd V2741) V2918) (if (= : V2742) (let V2743 (shen.lazyderef (tl V2741) V2918) (if (cons? V2743) (let V2744 (shen.lazyderef (hd V2743) V2918) (if (= string V2744) (let V2745 (shen.lazyderef (tl V2743) V2918) (if (= () V2745) (let Hyp (tl V2734) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons string ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2745) (do (shen.bindv V2745 () V2918) (let Result (let Hyp (tl V2734) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons string ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2745 V2918) Result))) false))) (if (shen.pvar? V2744) (do (shen.bindv V2744 string V2918) (let Result (let V2746 (shen.lazyderef (tl V2743) V2918) (if (= () V2746) (let Hyp (tl V2734) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons string ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (if (shen.pvar? V2746) (do (shen.bindv V2746 () V2918) (let Result (let Hyp (tl V2734) (do (shen.incinfs) (bind V2917 (cons (cons (shen.lazyderef X V2918) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2918) (cons : (cons string ()))) (shen.lazyderef Hyp V2918))) V2918 V2919))) (do (shen.unbindv V2746 V2918) Result))) false))) (do (shen.unbindv V2744 V2918) Result))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let V2747 (shen.lazyderef V2916 V2918) (if (cons? V2747) (let X (hd V2747) (let Hyp (tl V2747) (let NewHyps (shen.newpv V2918) (do (shen.incinfs) (bind V2917 (cons (shen.lazyderef X V2918) (shen.lazyderef NewHyps V2918)) V2918 (freeze (shen.t*-hyps Hyp NewHyps V2918 V2919))))))) false)) Case)) Case)) Case)) Case)))
+(defun shen.t*-hyps (V2824 V2825 V2826 V2827) (let Case (let V2579 (shen.lazyderef V2824 V2826) (if (cons? V2579) (let V2580 (shen.lazyderef (hd V2579) V2826) (if (cons? V2580) (let V2581 (shen.lazyderef (hd V2580) V2826) (if (cons? V2581) (let V2582 (shen.lazyderef (hd V2581) V2826) (if (= cons V2582) (let V2583 (shen.lazyderef (tl V2581) V2826) (if (cons? V2583) (let X (hd V2583) (let V2584 (shen.lazyderef (tl V2583) V2826) (if (cons? V2584) (let Y (hd V2584) (let V2585 (shen.lazyderef (tl V2584) V2826) (if (= () V2585) (let V2586 (shen.lazyderef (tl V2580) V2826) (if (cons? V2586) (let V2587 (shen.lazyderef (hd V2586) V2826) (if (= : V2587) (let V2588 (shen.lazyderef (tl V2586) V2826) (if (cons? V2588) (let V2589 (shen.lazyderef (hd V2588) V2826) (if (cons? V2589) (let V2590 (shen.lazyderef (hd V2589) V2826) (if (= list V2590) (let V2591 (shen.lazyderef (tl V2589) V2826) (if (cons? V2591) (let A (hd V2591) (let V2592 (shen.lazyderef (tl V2591) V2826) (if (= () V2592) (let V2593 (shen.lazyderef (tl V2588) V2826) (if (= () V2593) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2593) (do (shen.bindv V2593 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2593 V2826) Result))) false))) (if (shen.pvar? V2592) (do (shen.bindv V2592 () V2826) (let Result (let V2594 (shen.lazyderef (tl V2588) V2826) (if (= () V2594) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2594) (do (shen.bindv V2594 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2594 V2826) Result))) false))) (do (shen.unbindv V2592 V2826) Result))) false)))) (if (shen.pvar? V2591) (let A (shen.newpv V2826) (do (shen.bindv V2591 (cons A ()) V2826) (let Result (let V2595 (shen.lazyderef (tl V2588) V2826) (if (= () V2595) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2595) (do (shen.bindv V2595 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2595 V2826) Result))) false))) (do (shen.unbindv V2591 V2826) Result)))) false))) (if (shen.pvar? V2590) (do (shen.bindv V2590 list V2826) (let Result (let V2596 (shen.lazyderef (tl V2589) V2826) (if (cons? V2596) (let A (hd V2596) (let V2597 (shen.lazyderef (tl V2596) V2826) (if (= () V2597) (let V2598 (shen.lazyderef (tl V2588) V2826) (if (= () V2598) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2598) (do (shen.bindv V2598 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2598 V2826) Result))) false))) (if (shen.pvar? V2597) (do (shen.bindv V2597 () V2826) (let Result (let V2599 (shen.lazyderef (tl V2588) V2826) (if (= () V2599) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2599) (do (shen.bindv V2599 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2599 V2826) Result))) false))) (do (shen.unbindv V2597 V2826) Result))) false)))) (if (shen.pvar? V2596) (let A (shen.newpv V2826) (do (shen.bindv V2596 (cons A ()) V2826) (let Result (let V2600 (shen.lazyderef (tl V2588) V2826) (if (= () V2600) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2600) (do (shen.bindv V2600 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2600 V2826) Result))) false))) (do (shen.unbindv V2596 V2826) Result)))) false))) (do (shen.unbindv V2590 V2826) Result))) false))) (if (shen.pvar? V2589) (let A (shen.newpv V2826) (do (shen.bindv V2589 (cons list (cons A ())) V2826) (let Result (let V2601 (shen.lazyderef (tl V2588) V2826) (if (= () V2601) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2601) (do (shen.bindv V2601 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2601 V2826) Result))) false))) (do (shen.unbindv V2589 V2826) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2602 (shen.lazyderef V2824 V2826) (if (cons? V2602) (let V2603 (shen.lazyderef (hd V2602) V2826) (if (cons? V2603) (let V2604 (shen.lazyderef (hd V2603) V2826) (if (cons? V2604) (let V2605 (shen.lazyderef (hd V2604) V2826) (if (= @p V2605) (let V2606 (shen.lazyderef (tl V2604) V2826) (if (cons? V2606) (let X (hd V2606) (let V2607 (shen.lazyderef (tl V2606) V2826) (if (cons? V2607) (let Y (hd V2607) (let V2608 (shen.lazyderef (tl V2607) V2826) (if (= () V2608) (let V2609 (shen.lazyderef (tl V2603) V2826) (if (cons? V2609) (let V2610 (shen.lazyderef (hd V2609) V2826) (if (= : V2610) (let V2611 (shen.lazyderef (tl V2609) V2826) (if (cons? V2611) (let V2612 (shen.lazyderef (hd V2611) V2826) (if (cons? V2612) (let A (hd V2612) (let V2613 (shen.lazyderef (tl V2612) V2826) (if (cons? V2613) (let V2614 (shen.lazyderef (hd V2613) V2826) (if (= * V2614) (let V2615 (shen.lazyderef (tl V2613) V2826) (if (cons? V2615) (let B (hd V2615) (let V2616 (shen.lazyderef (tl V2615) V2826) (if (= () V2616) (let V2617 (shen.lazyderef (tl V2611) V2826) (if (= () V2617) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2617) (do (shen.bindv V2617 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2617 V2826) Result))) false))) (if (shen.pvar? V2616) (do (shen.bindv V2616 () V2826) (let Result (let V2618 (shen.lazyderef (tl V2611) V2826) (if (= () V2618) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2618) (do (shen.bindv V2618 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2618 V2826) Result))) false))) (do (shen.unbindv V2616 V2826) Result))) false)))) (if (shen.pvar? V2615) (let B (shen.newpv V2826) (do (shen.bindv V2615 (cons B ()) V2826) (let Result (let V2619 (shen.lazyderef (tl V2611) V2826) (if (= () V2619) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2619) (do (shen.bindv V2619 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2619 V2826) Result))) false))) (do (shen.unbindv V2615 V2826) Result)))) false))) (if (shen.pvar? V2614) (do (shen.bindv V2614 * V2826) (let Result (let V2620 (shen.lazyderef (tl V2613) V2826) (if (cons? V2620) (let B (hd V2620) (let V2621 (shen.lazyderef (tl V2620) V2826) (if (= () V2621) (let V2622 (shen.lazyderef (tl V2611) V2826) (if (= () V2622) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2622) (do (shen.bindv V2622 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2622 V2826) Result))) false))) (if (shen.pvar? V2621) (do (shen.bindv V2621 () V2826) (let Result (let V2623 (shen.lazyderef (tl V2611) V2826) (if (= () V2623) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2623) (do (shen.bindv V2623 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2623 V2826) Result))) false))) (do (shen.unbindv V2621 V2826) Result))) false)))) (if (shen.pvar? V2620) (let B (shen.newpv V2826) (do (shen.bindv V2620 (cons B ()) V2826) (let Result (let V2624 (shen.lazyderef (tl V2611) V2826) (if (= () V2624) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2624) (do (shen.bindv V2624 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2624 V2826) Result))) false))) (do (shen.unbindv V2620 V2826) Result)))) false))) (do (shen.unbindv V2614 V2826) Result))) false))) (if (shen.pvar? V2613) (let B (shen.newpv V2826) (do (shen.bindv V2613 (cons * (cons B ())) V2826) (let Result (let V2625 (shen.lazyderef (tl V2611) V2826) (if (= () V2625) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2625) (do (shen.bindv V2625 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2625 V2826) Result))) false))) (do (shen.unbindv V2613 V2826) Result)))) false)))) (if (shen.pvar? V2612) (let A (shen.newpv V2826) (let B (shen.newpv V2826) (do (shen.bindv V2612 (cons A (cons * (cons B ()))) V2826) (let Result (let V2626 (shen.lazyderef (tl V2611) V2826) (if (= () V2626) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2626) (do (shen.bindv V2626 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2626 V2826) Result))) false))) (do (shen.unbindv V2612 V2826) Result))))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2627 (shen.lazyderef V2824 V2826) (if (cons? V2627) (let V2628 (shen.lazyderef (hd V2627) V2826) (if (cons? V2628) (let V2629 (shen.lazyderef (hd V2628) V2826) (if (cons? V2629) (let V2630 (shen.lazyderef (hd V2629) V2826) (if (= @v V2630) (let V2631 (shen.lazyderef (tl V2629) V2826) (if (cons? V2631) (let X (hd V2631) (let V2632 (shen.lazyderef (tl V2631) V2826) (if (cons? V2632) (let Y (hd V2632) (let V2633 (shen.lazyderef (tl V2632) V2826) (if (= () V2633) (let V2634 (shen.lazyderef (tl V2628) V2826) (if (cons? V2634) (let V2635 (shen.lazyderef (hd V2634) V2826) (if (= : V2635) (let V2636 (shen.lazyderef (tl V2634) V2826) (if (cons? V2636) (let V2637 (shen.lazyderef (hd V2636) V2826) (if (cons? V2637) (let V2638 (shen.lazyderef (hd V2637) V2826) (if (= vector V2638) (let V2639 (shen.lazyderef (tl V2637) V2826) (if (cons? V2639) (let A (hd V2639) (let V2640 (shen.lazyderef (tl V2639) V2826) (if (= () V2640) (let V2641 (shen.lazyderef (tl V2636) V2826) (if (= () V2641) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2641) (do (shen.bindv V2641 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2641 V2826) Result))) false))) (if (shen.pvar? V2640) (do (shen.bindv V2640 () V2826) (let Result (let V2642 (shen.lazyderef (tl V2636) V2826) (if (= () V2642) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2642) (do (shen.bindv V2642 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2642 V2826) Result))) false))) (do (shen.unbindv V2640 V2826) Result))) false)))) (if (shen.pvar? V2639) (let A (shen.newpv V2826) (do (shen.bindv V2639 (cons A ()) V2826) (let Result (let V2643 (shen.lazyderef (tl V2636) V2826) (if (= () V2643) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2643) (do (shen.bindv V2643 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2643 V2826) Result))) false))) (do (shen.unbindv V2639 V2826) Result)))) false))) (if (shen.pvar? V2638) (do (shen.bindv V2638 vector V2826) (let Result (let V2644 (shen.lazyderef (tl V2637) V2826) (if (cons? V2644) (let A (hd V2644) (let V2645 (shen.lazyderef (tl V2644) V2826) (if (= () V2645) (let V2646 (shen.lazyderef (tl V2636) V2826) (if (= () V2646) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2646) (do (shen.bindv V2646 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2646 V2826) Result))) false))) (if (shen.pvar? V2645) (do (shen.bindv V2645 () V2826) (let Result (let V2647 (shen.lazyderef (tl V2636) V2826) (if (= () V2647) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2647) (do (shen.bindv V2647 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2647 V2826) Result))) false))) (do (shen.unbindv V2645 V2826) Result))) false)))) (if (shen.pvar? V2644) (let A (shen.newpv V2826) (do (shen.bindv V2644 (cons A ()) V2826) (let Result (let V2648 (shen.lazyderef (tl V2636) V2826) (if (= () V2648) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2648) (do (shen.bindv V2648 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2648 V2826) Result))) false))) (do (shen.unbindv V2644 V2826) Result)))) false))) (do (shen.unbindv V2638 V2826) Result))) false))) (if (shen.pvar? V2637) (let A (shen.newpv V2826) (do (shen.bindv V2637 (cons vector (cons A ())) V2826) (let Result (let V2649 (shen.lazyderef (tl V2636) V2826) (if (= () V2649) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2649) (do (shen.bindv V2649 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2649 V2826) Result))) false))) (do (shen.unbindv V2637 V2826) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2650 (shen.lazyderef V2824 V2826) (if (cons? V2650) (let V2651 (shen.lazyderef (hd V2650) V2826) (if (cons? V2651) (let V2652 (shen.lazyderef (hd V2651) V2826) (if (cons? V2652) (let V2653 (shen.lazyderef (hd V2652) V2826) (if (= @s V2653) (let V2654 (shen.lazyderef (tl V2652) V2826) (if (cons? V2654) (let X (hd V2654) (let V2655 (shen.lazyderef (tl V2654) V2826) (if (cons? V2655) (let Y (hd V2655) (let V2656 (shen.lazyderef (tl V2655) V2826) (if (= () V2656) (let V2657 (shen.lazyderef (tl V2651) V2826) (if (cons? V2657) (let V2658 (shen.lazyderef (hd V2657) V2826) (if (= : V2658) (let V2659 (shen.lazyderef (tl V2657) V2826) (if (cons? V2659) (let V2660 (shen.lazyderef (hd V2659) V2826) (if (= string V2660) (let V2661 (shen.lazyderef (tl V2659) V2826) (if (= () V2661) (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2661) (do (shen.bindv V2661 () V2826) (let Result (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2661 V2826) Result))) false))) (if (shen.pvar? V2660) (do (shen.bindv V2660 string V2826) (let Result (let V2662 (shen.lazyderef (tl V2659) V2826) (if (= () V2662) (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2662) (do (shen.bindv V2662 () V2826) (let Result (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2662 V2826) Result))) false))) (do (shen.unbindv V2660 V2826) Result))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let V2663 (shen.lazyderef V2824 V2826) (if (cons? V2663) (let X (hd V2663) (let Hyp (tl V2663) (let NewHyps (shen.newpv V2826) (do (shen.incinfs) (bind V2825 (cons (shen.lazyderef X V2826) (shen.lazyderef NewHyps V2826)) V2826 (freeze (shen.t*-hyps Hyp NewHyps V2826 V2827))))))) false)) Case)) Case)) Case)) Case)))
 
-(defun shen.show (V2932 V2933 V2934 V2935) (cond ((value shen.*spy*) (do (shen.line) (do (shen.show-p (shen.deref V2932 V2934)) (do (nl 1) (do (nl 1) (do (shen.show-assumptions (shen.deref V2933 V2934) 1) (do (shen.prhush "
-> " (stoutput)) (do (shen.pause-for-user) (thaw V2935))))))))) (true (thaw V2935))))
+(defun shen.show (V2840 V2841 V2842 V2843) (cond ((value shen.*spy*) (do (shen.line) (do (shen.show-p (shen.deref V2840 V2842)) (do (nl 1) (do (nl 1) (do (shen.show-assumptions (shen.deref V2841 V2842) 1) (do (shen.prhush "
+> " (stoutput)) (do (shen.pause-for-user) (thaw V2843))))))))) (true (thaw V2843))))
 
 (defun shen.line () (let Infs (inferences) (shen.prhush (cn "____________________________________________________________ " (shen.app Infs (cn " inference" (shen.app (if (= 1 Infs) "" "s") " 
 ?- " shen.a)) shen.a)) (stoutput))))
 
-(defun shen.show-p (V2936) (cond ((and (cons? V2936) (and (cons? (tl V2936)) (and (= : (hd (tl V2936))) (and (cons? (tl (tl V2936))) (= () (tl (tl (tl V2936)))))))) (shen.prhush (shen.app (hd V2936) (cn " : " (shen.app (hd (tl (tl V2936))) "" shen.r)) shen.r) (stoutput))) (true (shen.prhush (shen.app V2936 "" shen.r) (stoutput)))))
+(defun shen.show-p (V2844) (cond ((and (cons? V2844) (and (cons? (tl V2844)) (and (= : (hd (tl V2844))) (and (cons? (tl (tl V2844))) (= () (tl (tl (tl V2844)))))))) (shen.prhush (shen.app (hd V2844) (cn " : " (shen.app (hd (tl (tl V2844))) "" shen.r)) shen.r) (stoutput))) (true (shen.prhush (shen.app V2844 "" shen.r) (stoutput)))))
 
-(defun shen.show-assumptions (V2939 V2940) (cond ((= () V2939) shen.skip) ((cons? V2939) (do (shen.prhush (shen.app V2940 ". " shen.a) (stoutput)) (do (shen.show-p (hd V2939)) (do (nl 1) (shen.show-assumptions (tl V2939) (+ V2940 1)))))) (true (shen.sys-error shen.show-assumptions))))
+(defun shen.show-assumptions (V2847 V2848) (cond ((= () V2847) shen.skip) ((cons? V2847) (do (shen.prhush (shen.app V2848 ". " shen.a) (stoutput)) (do (shen.show-p (hd V2847)) (do (nl 1) (shen.show-assumptions (tl V2847) (+ V2848 1)))))) (true (shen.sys-error shen.show-assumptions))))
 
 (defun shen.pause-for-user () (let Byte (read-byte (stinput)) (if (= Byte 94) (simple-error "input aborted
 ") (nl 1))))
 
-(defun shen.typedf? (V2941) (cons? (assoc V2941 (value shen.*signedfuncs*))))
+(defun shen.typedf? (V2849) (cons? (assoc V2849 (value shen.*signedfuncs*))))
 
-(defun shen.sigf (V2942) (concat shen.type-signature-of- V2942))
+(defun shen.sigf (V2850) (concat shen.type-signature-of- V2850))
 
 (defun shen.placeholder () (gensym &&))
 
-(defun shen.base (V2943 V2944 V2945 V2946) (let Case (let V2650 (shen.lazyderef V2944 V2945) (if (= number V2650) (do (shen.incinfs) (fwhen (number? (shen.lazyderef V2943 V2945)) V2945 V2946)) (if (shen.pvar? V2650) (do (shen.bindv V2650 number V2945) (let Result (do (shen.incinfs) (fwhen (number? (shen.lazyderef V2943 V2945)) V2945 V2946)) (do (shen.unbindv V2650 V2945) Result))) false))) (if (= Case false) (let Case (let V2651 (shen.lazyderef V2944 V2945) (if (= boolean V2651) (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V2943 V2945)) V2945 V2946)) (if (shen.pvar? V2651) (do (shen.bindv V2651 boolean V2945) (let Result (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V2943 V2945)) V2945 V2946)) (do (shen.unbindv V2651 V2945) Result))) false))) (if (= Case false) (let Case (let V2652 (shen.lazyderef V2944 V2945) (if (= string V2652) (do (shen.incinfs) (fwhen (string? (shen.lazyderef V2943 V2945)) V2945 V2946)) (if (shen.pvar? V2652) (do (shen.bindv V2652 string V2945) (let Result (do (shen.incinfs) (fwhen (string? (shen.lazyderef V2943 V2945)) V2945 V2946)) (do (shen.unbindv V2652 V2945) Result))) false))) (if (= Case false) (let Case (let V2653 (shen.lazyderef V2944 V2945) (if (= symbol V2653) (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V2943 V2945)) V2945 (freeze (fwhen (not (shen.ue? (shen.lazyderef V2943 V2945))) V2945 V2946)))) (if (shen.pvar? V2653) (do (shen.bindv V2653 symbol V2945) (let Result (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V2943 V2945)) V2945 (freeze (fwhen (not (shen.ue? (shen.lazyderef V2943 V2945))) V2945 V2946)))) (do (shen.unbindv V2653 V2945) Result))) false))) (if (= Case false) (let V2654 (shen.lazyderef V2943 V2945) (if (= () V2654) (let V2655 (shen.lazyderef V2944 V2945) (if (cons? V2655) (let V2656 (shen.lazyderef (hd V2655) V2945) (if (= list V2656) (let V2657 (shen.lazyderef (tl V2655) V2945) (if (cons? V2657) (let A (hd V2657) (let V2658 (shen.lazyderef (tl V2657) V2945) (if (= () V2658) (do (shen.incinfs) (thaw V2946)) (if (shen.pvar? V2658) (do (shen.bindv V2658 () V2945) (let Result (do (shen.incinfs) (thaw V2946)) (do (shen.unbindv V2658 V2945) Result))) false)))) (if (shen.pvar? V2657) (let A (shen.newpv V2945) (do (shen.bindv V2657 (cons A ()) V2945) (let Result (do (shen.incinfs) (thaw V2946)) (do (shen.unbindv V2657 V2945) Result)))) false))) (if (shen.pvar? V2656) (do (shen.bindv V2656 list V2945) (let Result (let V2659 (shen.lazyderef (tl V2655) V2945) (if (cons? V2659) (let A (hd V2659) (let V2660 (shen.lazyderef (tl V2659) V2945) (if (= () V2660) (do (shen.incinfs) (thaw V2946)) (if (shen.pvar? V2660) (do (shen.bindv V2660 () V2945) (let Result (do (shen.incinfs) (thaw V2946)) (do (shen.unbindv V2660 V2945) Result))) false)))) (if (shen.pvar? V2659) (let A (shen.newpv V2945) (do (shen.bindv V2659 (cons A ()) V2945) (let Result (do (shen.incinfs) (thaw V2946)) (do (shen.unbindv V2659 V2945) Result)))) false))) (do (shen.unbindv V2656 V2945) Result))) false))) (if (shen.pvar? V2655) (let A (shen.newpv V2945) (do (shen.bindv V2655 (cons list (cons A ())) V2945) (let Result (do (shen.incinfs) (thaw V2946)) (do (shen.unbindv V2655 V2945) Result)))) false))) false)) Case)) Case)) Case)) Case)))
+(defun shen.base (V2851 V2852 V2853 V2854) (let Case (let V2566 (shen.lazyderef V2852 V2853) (if (= number V2566) (do (shen.incinfs) (fwhen (number? (shen.lazyderef V2851 V2853)) V2853 V2854)) (if (shen.pvar? V2566) (do (shen.bindv V2566 number V2853) (let Result (do (shen.incinfs) (fwhen (number? (shen.lazyderef V2851 V2853)) V2853 V2854)) (do (shen.unbindv V2566 V2853) Result))) false))) (if (= Case false) (let Case (let V2567 (shen.lazyderef V2852 V2853) (if (= boolean V2567) (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V2851 V2853)) V2853 V2854)) (if (shen.pvar? V2567) (do (shen.bindv V2567 boolean V2853) (let Result (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V2851 V2853)) V2853 V2854)) (do (shen.unbindv V2567 V2853) Result))) false))) (if (= Case false) (let Case (let V2568 (shen.lazyderef V2852 V2853) (if (= string V2568) (do (shen.incinfs) (fwhen (string? (shen.lazyderef V2851 V2853)) V2853 V2854)) (if (shen.pvar? V2568) (do (shen.bindv V2568 string V2853) (let Result (do (shen.incinfs) (fwhen (string? (shen.lazyderef V2851 V2853)) V2853 V2854)) (do (shen.unbindv V2568 V2853) Result))) false))) (if (= Case false) (let Case (let V2569 (shen.lazyderef V2852 V2853) (if (= symbol V2569) (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V2851 V2853)) V2853 (freeze (fwhen (not (shen.ue? (shen.lazyderef V2851 V2853))) V2853 V2854)))) (if (shen.pvar? V2569) (do (shen.bindv V2569 symbol V2853) (let Result (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V2851 V2853)) V2853 (freeze (fwhen (not (shen.ue? (shen.lazyderef V2851 V2853))) V2853 V2854)))) (do (shen.unbindv V2569 V2853) Result))) false))) (if (= Case false) (let V2570 (shen.lazyderef V2851 V2853) (if (= () V2570) (let V2571 (shen.lazyderef V2852 V2853) (if (cons? V2571) (let V2572 (shen.lazyderef (hd V2571) V2853) (if (= list V2572) (let V2573 (shen.lazyderef (tl V2571) V2853) (if (cons? V2573) (let A (hd V2573) (let V2574 (shen.lazyderef (tl V2573) V2853) (if (= () V2574) (do (shen.incinfs) (thaw V2854)) (if (shen.pvar? V2574) (do (shen.bindv V2574 () V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2574 V2853) Result))) false)))) (if (shen.pvar? V2573) (let A (shen.newpv V2853) (do (shen.bindv V2573 (cons A ()) V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2573 V2853) Result)))) false))) (if (shen.pvar? V2572) (do (shen.bindv V2572 list V2853) (let Result (let V2575 (shen.lazyderef (tl V2571) V2853) (if (cons? V2575) (let A (hd V2575) (let V2576 (shen.lazyderef (tl V2575) V2853) (if (= () V2576) (do (shen.incinfs) (thaw V2854)) (if (shen.pvar? V2576) (do (shen.bindv V2576 () V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2576 V2853) Result))) false)))) (if (shen.pvar? V2575) (let A (shen.newpv V2853) (do (shen.bindv V2575 (cons A ()) V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2575 V2853) Result)))) false))) (do (shen.unbindv V2572 V2853) Result))) false))) (if (shen.pvar? V2571) (let A (shen.newpv V2853) (do (shen.bindv V2571 (cons list (cons A ())) V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2571 V2853) Result)))) false))) false)) Case)) Case)) Case)) Case)))
 
-(defun shen.by_hypothesis (V2947 V2948 V2949 V2950 V2951) (let Case (let V2641 (shen.lazyderef V2949 V2950) (if (cons? V2641) (let V2642 (shen.lazyderef (hd V2641) V2950) (if (cons? V2642) (let Y (hd V2642) (let V2643 (shen.lazyderef (tl V2642) V2950) (if (cons? V2643) (let V2644 (shen.lazyderef (hd V2643) V2950) (if (= : V2644) (let V2645 (shen.lazyderef (tl V2643) V2950) (if (cons? V2645) (let B (hd V2645) (let V2646 (shen.lazyderef (tl V2645) V2950) (if (= () V2646) (do (shen.incinfs) (identical V2947 Y V2950 (freeze (unify! V2948 B V2950 V2951)))) false))) false)) false)) false))) false)) false)) (if (= Case false) (let V2647 (shen.lazyderef V2949 V2950) (if (cons? V2647) (let Hyp (tl V2647) (do (shen.incinfs) (shen.by_hypothesis V2947 V2948 Hyp V2950 V2951))) false)) Case)))
+(defun shen.by_hypothesis (V2855 V2856 V2857 V2858 V2859) (let Case (let V2557 (shen.lazyderef V2857 V2858) (if (cons? V2557) (let V2558 (shen.lazyderef (hd V2557) V2858) (if (cons? V2558) (let Y (hd V2558) (let V2559 (shen.lazyderef (tl V2558) V2858) (if (cons? V2559) (let V2560 (shen.lazyderef (hd V2559) V2858) (if (= : V2560) (let V2561 (shen.lazyderef (tl V2559) V2858) (if (cons? V2561) (let B (hd V2561) (let V2562 (shen.lazyderef (tl V2561) V2858) (if (= () V2562) (do (shen.incinfs) (identical V2855 Y V2858 (freeze (unify! V2856 B V2858 V2859)))) false))) false)) false)) false))) false)) false)) (if (= Case false) (let V2563 (shen.lazyderef V2857 V2858) (if (cons? V2563) (let Hyp (tl V2563) (do (shen.incinfs) (shen.by_hypothesis V2855 V2856 Hyp V2858 V2859))) false)) Case)))
 
-(defun shen.t*-def (V2952 V2953 V2954 V2955 V2956) (let V2635 (shen.lazyderef V2952 V2955) (if (cons? V2635) (let V2636 (shen.lazyderef (hd V2635) V2955) (if (= define V2636) (let V2637 (shen.lazyderef (tl V2635) V2955) (if (cons? V2637) (let F (hd V2637) (let X (tl V2637) (let E (shen.newpv V2955) (do (shen.incinfs) (shen.t*-defh (compile (lambda X2878 (shen.<sig+rules> X2878)) X (lambda E (if (cons? E) (simple-error (cn "parse error here: " (shen.app E "
+(defun shen.t*-def (V2860 V2861 V2862 V2863 V2864) (let V2551 (shen.lazyderef V2860 V2863) (if (cons? V2551) (let V2552 (shen.lazyderef (hd V2551) V2863) (if (= define V2552) (let V2553 (shen.lazyderef (tl V2551) V2863) (if (cons? V2553) (let F (hd V2553) (let X (tl V2553) (let E (shen.newpv V2863) (do (shen.incinfs) (shen.t*-defh (compile (lambda X2787 (shen.<sig+rules> X2787)) X (lambda E (if (cons? E) (simple-error (cn "parse error here: " (shen.app E "
 " shen.s))) (simple-error "parse error
-")))) F V2953 V2954 V2955 V2956))))) false)) false)) false)))
+")))) F V2861 V2862 V2863 V2864))))) false)) false)) false)))
 
-(defun shen.t*-defh (V2957 V2958 V2959 V2960 V2961 V2962) (let V2631 (shen.lazyderef V2957 V2961) (if (cons? V2631) (let Sig (hd V2631) (let Rules (tl V2631) (do (shen.incinfs) (shen.t*-defhh Sig (shen.ue-sig Sig) V2958 V2959 V2960 Rules V2961 V2962)))) false)))
+(defun shen.t*-defh (V2865 V2866 V2867 V2868 V2869 V2870) (let V2547 (shen.lazyderef V2865 V2869) (if (cons? V2547) (let Sig (hd V2547) (let Rules (tl V2547) (do (shen.incinfs) (shen.t*-defhh Sig (shen.ue-sig Sig) V2866 V2867 V2868 Rules V2869 V2870)))) false)))
 
-(defun shen.t*-defhh (V2963 V2964 V2965 V2966 V2967 V2968 V2969 V2970) (do (shen.incinfs) (shen.t*-rules V2968 V2964 1 V2965 (cons (cons V2965 (cons : (cons V2964 ()))) V2967) V2969 (freeze (shen.memo V2965 V2963 V2966 V2969 V2970)))))
+(defun shen.t*-defhh (V2871 V2872 V2873 V2874 V2875 V2876 V2877 V2878) (do (shen.incinfs) (shen.t*-rules V2876 V2872 1 V2873 (cons (cons V2873 (cons : (cons V2872 ()))) V2875) V2877 (freeze (shen.memo V2873 V2871 V2874 V2877 V2878)))))
 
-(defun shen.memo (V2971 V2972 V2973 V2974 V2975) (let Jnk (shen.newpv V2974) (do (shen.incinfs) (unify! V2973 V2972 V2974 (freeze (bind Jnk (declare (shen.lazyderef V2971 V2974) (shen.lazyderef V2973 V2974)) V2974 V2975))))))
+(defun shen.memo (V2879 V2880 V2881 V2882 V2883) (let Jnk (shen.newpv V2882) (do (shen.incinfs) (unify! V2881 V2880 V2882 (freeze (bind Jnk (declare (shen.lazyderef V2879 V2882) (shen.lazyderef V2881 V2882)) V2882 V2883))))))
 
-(defun shen.<sig+rules> (V2980) (let Result (let Parse_shen.<signature> (shen.<signature> V2980) (if (not (= (fail) Parse_shen.<signature>)) (let Parse_shen.<rules> (shen.<rules> Parse_shen.<signature>) (if (not (= (fail) Parse_shen.<rules>)) (shen.pair (hd Parse_shen.<rules>) (cons (shen.hdtl Parse_shen.<signature>) (shen.hdtl Parse_shen.<rules>))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)))
+(defun shen.<sig+rules> (V2888) (let Result (let Parse_shen.<signature> (shen.<signature> V2888) (if (not (= (fail) Parse_shen.<signature>)) (let Parse_shen.<rules> (shen.<rules> Parse_shen.<signature>) (if (not (= (fail) Parse_shen.<rules>)) (shen.pair (hd Parse_shen.<rules>) (cons (shen.hdtl Parse_shen.<signature>) (shen.hdtl Parse_shen.<rules>))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)))
 
-(defun shen.ue (V2981) (cond ((and (cons? V2981) (and (cons? (tl V2981)) (and (= () (tl (tl V2981))) (= (hd V2981) protect)))) V2981) ((cons? V2981) (map (lambda X2879 (shen.ue X2879)) V2981)) ((variable? V2981) (concat && V2981)) (true V2981)))
+(defun shen.ue (V2889) (cond ((and (cons? V2889) (and (cons? (tl V2889)) (and (= () (tl (tl V2889))) (= (hd V2889) protect)))) V2889) ((cons? V2889) (map (lambda X2788 (shen.ue X2788)) V2889)) ((variable? V2889) (concat && V2889)) (true V2889)))
 
-(defun shen.ue-sig (V2982) (cond ((cons? V2982) (map (lambda X2880 (shen.ue-sig X2880)) V2982)) ((variable? V2982) (concat &&& V2982)) (true V2982)))
+(defun shen.ue-sig (V2890) (cond ((cons? V2890) (map (lambda X2789 (shen.ue-sig X2789)) V2890)) ((variable? V2890) (concat &&& V2890)) (true V2890)))
 
-(defun shen.ues (V2987) (cond ((shen.ue? V2987) (cons V2987 ())) ((cons? V2987) (union (shen.ues (hd V2987)) (shen.ues (tl V2987)))) (true ())))
+(defun shen.ues (V2895) (cond ((shen.ue? V2895) (cons V2895 ())) ((cons? V2895) (union (shen.ues (hd V2895)) (shen.ues (tl V2895)))) (true ())))
 
-(defun shen.ue? (V2988) (and (symbol? V2988) (shen.ue-h? (str V2988))))
+(defun shen.ue? (V2896) (and (symbol? V2896) (shen.ue-h? (str V2896))))
 
-(defun shen.ue-h? (V2995) (cond ((and (shen.+string? V2995) (and (= "&" (pos V2995 0)) (and (shen.+string? (tlstr V2995)) (= "&" (pos (tlstr V2995) 0))))) true) (true false)))
+(defun shen.ue-h? (V2903) (cond ((and (shen.+string? V2903) (and (= "&" (pos V2903 0)) (and (shen.+string? (tlstr V2903)) (= "&" (pos (tlstr V2903) 0))))) true) (true false)))
 
-(defun shen.t*-rules (V2996 V2997 V2998 V2999 V3000 V3001 V3002) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2606 (shen.lazyderef V2996 V3001) (if (= () V2606) (do (shen.incinfs) (thaw V3002)) false)) (if (= Case false) (let Case (let V2607 (shen.lazyderef V2996 V3001) (if (cons? V2607) (let V2608 (shen.lazyderef (hd V2607) V3001) (if (cons? V2608) (let V2609 (shen.lazyderef (hd V2608) V3001) (if (= () V2609) (let V2610 (shen.lazyderef (tl V2608) V3001) (if (cons? V2610) (let Action (hd V2610) (let V2611 (shen.lazyderef (tl V2610) V3001) (if (= () V2611) (let Rules (tl V2607) (let V2612 (shen.lazyderef V2997 V3001) (if (cons? V2612) (let V2613 (shen.lazyderef (hd V2612) V3001) (if (= --> V2613) (let V2614 (shen.lazyderef (tl V2612) V3001) (if (cons? V2614) (let A (hd V2614) (let V2615 (shen.lazyderef (tl V2614) V3001) (if (= () V2615) (do (shen.incinfs) (shen.t*-rule (cons () (cons (shen.ue Action) ())) A V3000 V3001 (freeze (cut Throwcontrol V3001 (freeze (shen.t*-rules Rules A (+ V2998 1) V2999 V3000 V3001 V3002)))))) false))) false)) false)) false))) false))) false)) false)) false)) false)) (if (= Case false) (let Case (let V2616 (shen.lazyderef V2996 V3001) (if (cons? V2616) (let Rule (hd V2616) (let Rules (tl V2616) (do (shen.incinfs) (shen.t*-rule (shen.ue Rule) V2997 V3000 V3001 (freeze (cut Throwcontrol V3001 (freeze (shen.t*-rules Rules V2997 (+ V2998 1) V2999 V3000 V3001 V3002)))))))) false)) (if (= Case false) (let Err (shen.newpv V3001) (do (shen.incinfs) (bind Err (simple-error (cn "type error in rule " (shen.app (shen.lazyderef V2998 V3001) (cn " of " (shen.app (shen.lazyderef V2999 V3001) "" shen.a)) shen.a))) V3001 V3002))) Case)) Case)) Case)))))
+(defun shen.t*-rules (V2904 V2905 V2906 V2907 V2908 V2909 V2910) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2522 (shen.lazyderef V2904 V2909) (if (= () V2522) (do (shen.incinfs) (thaw V2910)) false)) (if (= Case false) (let Case (let V2523 (shen.lazyderef V2904 V2909) (if (cons? V2523) (let V2524 (shen.lazyderef (hd V2523) V2909) (if (cons? V2524) (let V2525 (shen.lazyderef (hd V2524) V2909) (if (= () V2525) (let V2526 (shen.lazyderef (tl V2524) V2909) (if (cons? V2526) (let Action (hd V2526) (let V2527 (shen.lazyderef (tl V2526) V2909) (if (= () V2527) (let Rules (tl V2523) (let V2528 (shen.lazyderef V2905 V2909) (if (cons? V2528) (let V2529 (shen.lazyderef (hd V2528) V2909) (if (= --> V2529) (let V2530 (shen.lazyderef (tl V2528) V2909) (if (cons? V2530) (let A (hd V2530) (let V2531 (shen.lazyderef (tl V2530) V2909) (if (= () V2531) (do (shen.incinfs) (shen.t*-rule (cons () (cons (shen.ue Action) ())) A V2908 V2909 (freeze (cut Throwcontrol V2909 (freeze (shen.t*-rules Rules A (+ V2906 1) V2907 V2908 V2909 V2910)))))) false))) false)) false)) false))) false))) false)) false)) false)) false)) (if (= Case false) (let Case (let V2532 (shen.lazyderef V2904 V2909) (if (cons? V2532) (let Rule (hd V2532) (let Rules (tl V2532) (do (shen.incinfs) (shen.t*-rule (shen.ue Rule) V2905 V2908 V2909 (freeze (cut Throwcontrol V2909 (freeze (shen.t*-rules Rules V2905 (+ V2906 1) V2907 V2908 V2909 V2910)))))))) false)) (if (= Case false) (let Err (shen.newpv V2909) (do (shen.incinfs) (bind Err (simple-error (cn "type error in rule " (shen.app (shen.lazyderef V2906 V2909) (cn " of " (shen.app (shen.lazyderef V2907 V2909) "" shen.a)) shen.a))) V2909 V2910))) Case)) Case)) Case)))))
 
-(defun shen.t*-rule (V3003 V3004 V3005 V3006 V3007) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2588 (shen.lazyderef V3003 V3006) (if (cons? V2588) (let V2589 (shen.lazyderef (hd V2588) V3006) (if (= () V2589) (let V2590 (shen.lazyderef (tl V2588) V3006) (if (cons? V2590) (let Action (hd V2590) (let V2591 (shen.lazyderef (tl V2590) V3006) (if (= () V2591) (do (shen.incinfs) (cut Throwcontrol V3006 (freeze (shen.t*-action (shen.curry Action) V3004 V3005 V3006 V3007)))) false))) false)) false)) false)) (if (= Case false) (let V2592 (shen.lazyderef V3003 V3006) (if (cons? V2592) (let V2593 (shen.lazyderef (hd V2592) V3006) (if (cons? V2593) (let Pattern (hd V2593) (let Patterns (tl V2593) (let V2594 (shen.lazyderef (tl V2592) V3006) (if (cons? V2594) (let Action (hd V2594) (let V2595 (shen.lazyderef (tl V2594) V3006) (if (= () V2595) (let V2596 (shen.lazyderef V3004 V3006) (if (cons? V2596) (let A (hd V2596) (let V2597 (shen.lazyderef (tl V2596) V3006) (if (cons? V2597) (let V2598 (shen.lazyderef (hd V2597) V3006) (if (= --> V2598) (let V2599 (shen.lazyderef (tl V2597) V3006) (if (cons? V2599) (let B (hd V2599) (let V2600 (shen.lazyderef (tl V2599) V3006) (if (= () V2600) (do (shen.incinfs) (shen.t*-pattern Pattern A V3006 (freeze (cut Throwcontrol V3006 (freeze (shen.t*-rule (cons Patterns (cons Action ())) B (cons (cons Pattern (cons : (cons A ()))) V3005) V3006 V3007)))))) false))) false)) false)) false))) false)) false))) false)))) false)) false)) Case)))))
+(defun shen.t*-rule (V2911 V2912 V2913 V2914 V2915) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2504 (shen.lazyderef V2911 V2914) (if (cons? V2504) (let V2505 (shen.lazyderef (hd V2504) V2914) (if (= () V2505) (let V2506 (shen.lazyderef (tl V2504) V2914) (if (cons? V2506) (let Action (hd V2506) (let V2507 (shen.lazyderef (tl V2506) V2914) (if (= () V2507) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (shen.t*-action (shen.curry Action) V2912 V2913 V2914 V2915)))) false))) false)) false)) false)) (if (= Case false) (let V2508 (shen.lazyderef V2911 V2914) (if (cons? V2508) (let V2509 (shen.lazyderef (hd V2508) V2914) (if (cons? V2509) (let Pattern (hd V2509) (let Patterns (tl V2509) (let V2510 (shen.lazyderef (tl V2508) V2914) (if (cons? V2510) (let Action (hd V2510) (let V2511 (shen.lazyderef (tl V2510) V2914) (if (= () V2511) (let V2512 (shen.lazyderef V2912 V2914) (if (cons? V2512) (let A (hd V2512) (let V2513 (shen.lazyderef (tl V2512) V2914) (if (cons? V2513) (let V2514 (shen.lazyderef (hd V2513) V2914) (if (= --> V2514) (let V2515 (shen.lazyderef (tl V2513) V2914) (if (cons? V2515) (let B (hd V2515) (let V2516 (shen.lazyderef (tl V2515) V2914) (if (= () V2516) (do (shen.incinfs) (shen.t*-pattern Pattern A V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.t*-rule (cons Patterns (cons Action ())) B (cons (cons Pattern (cons : (cons A ()))) V2913) V2914 V2915)))))) false))) false)) false)) false))) false)) false))) false)))) false)) false)) Case)))))
 
-(defun shen.t*-action (V3008 V3009 V3010 V3011 V3012) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2565 (shen.lazyderef V3008 V3011) (if (cons? V2565) (let V2566 (shen.lazyderef (hd V2565) V3011) (if (= where V2566) (let V2567 (shen.lazyderef (tl V2565) V3011) (if (cons? V2567) (let P (hd V2567) (let V2568 (shen.lazyderef (tl V2567) V3011) (if (cons? V2568) (let Action (hd V2568) (let V2569 (shen.lazyderef (tl V2568) V3011) (if (= () V2569) (do (shen.incinfs) (cut Throwcontrol V3011 (freeze (shen.t* (cons P (cons : (cons boolean ()))) V3010 V3011 (freeze (cut Throwcontrol V3011 (freeze (shen.t*-action Action V3009 (cons (cons P (cons : (cons verified ()))) V3010) V3011 V3012)))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2570 (shen.lazyderef V3008 V3011) (if (cons? V2570) (let V2571 (shen.lazyderef (hd V2570) V3011) (if (= shen.choicepoint! V2571) (let V2572 (shen.lazyderef (tl V2570) V3011) (if (cons? V2572) (let V2573 (shen.lazyderef (hd V2572) V3011) (if (cons? V2573) (let V2574 (shen.lazyderef (hd V2573) V3011) (if (cons? V2574) (let V2575 (shen.lazyderef (hd V2574) V3011) (if (= fail-if V2575) (let V2576 (shen.lazyderef (tl V2574) V3011) (if (cons? V2576) (let F (hd V2576) (let V2577 (shen.lazyderef (tl V2576) V3011) (if (= () V2577) (let V2578 (shen.lazyderef (tl V2573) V3011) (if (cons? V2578) (let Action (hd V2578) (let V2579 (shen.lazyderef (tl V2578) V3011) (if (= () V2579) (let V2580 (shen.lazyderef (tl V2572) V3011) (if (= () V2580) (do (shen.incinfs) (cut Throwcontrol V3011 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons F (cons Action ())) ())) (cons Action ()))) V3009 V3010 V3011 V3012)))) false)) false))) false)) false))) false)) false)) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2581 (shen.lazyderef V3008 V3011) (if (cons? V2581) (let V2582 (shen.lazyderef (hd V2581) V3011) (if (= shen.choicepoint! V2582) (let V2583 (shen.lazyderef (tl V2581) V3011) (if (cons? V2583) (let Action (hd V2583) (let V2584 (shen.lazyderef (tl V2583) V3011) (if (= () V2584) (do (shen.incinfs) (cut Throwcontrol V3011 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons (cons = (cons Action ())) (cons (cons fail ()) ())) ())) (cons Action ()))) V3009 V3010 V3011 V3012)))) false))) false)) false)) false)) (if (= Case false) (do (shen.incinfs) (shen.t* (cons V3008 (cons : (cons V3009 ()))) V3010 V3011 V3012)) Case)) Case)) Case)))))
+(defun shen.t*-action (V2916 V2917 V2918 V2919 V2920) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2481 (shen.lazyderef V2916 V2919) (if (cons? V2481) (let V2482 (shen.lazyderef (hd V2481) V2919) (if (= where V2482) (let V2483 (shen.lazyderef (tl V2481) V2919) (if (cons? V2483) (let P (hd V2483) (let V2484 (shen.lazyderef (tl V2483) V2919) (if (cons? V2484) (let Action (hd V2484) (let V2485 (shen.lazyderef (tl V2484) V2919) (if (= () V2485) (do (shen.incinfs) (cut Throwcontrol V2919 (freeze (shen.t* (cons P (cons : (cons boolean ()))) V2918 V2919 (freeze (cut Throwcontrol V2919 (freeze (shen.t*-action Action V2917 (cons (cons P (cons : (cons verified ()))) V2918) V2919 V2920)))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2486 (shen.lazyderef V2916 V2919) (if (cons? V2486) (let V2487 (shen.lazyderef (hd V2486) V2919) (if (= shen.choicepoint! V2487) (let V2488 (shen.lazyderef (tl V2486) V2919) (if (cons? V2488) (let V2489 (shen.lazyderef (hd V2488) V2919) (if (cons? V2489) (let V2490 (shen.lazyderef (hd V2489) V2919) (if (cons? V2490) (let V2491 (shen.lazyderef (hd V2490) V2919) (if (= fail-if V2491) (let V2492 (shen.lazyderef (tl V2490) V2919) (if (cons? V2492) (let F (hd V2492) (let V2493 (shen.lazyderef (tl V2492) V2919) (if (= () V2493) (let V2494 (shen.lazyderef (tl V2489) V2919) (if (cons? V2494) (let Action (hd V2494) (let V2495 (shen.lazyderef (tl V2494) V2919) (if (= () V2495) (let V2496 (shen.lazyderef (tl V2488) V2919) (if (= () V2496) (do (shen.incinfs) (cut Throwcontrol V2919 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons F (cons Action ())) ())) (cons Action ()))) V2917 V2918 V2919 V2920)))) false)) false))) false)) false))) false)) false)) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2497 (shen.lazyderef V2916 V2919) (if (cons? V2497) (let V2498 (shen.lazyderef (hd V2497) V2919) (if (= shen.choicepoint! V2498) (let V2499 (shen.lazyderef (tl V2497) V2919) (if (cons? V2499) (let Action (hd V2499) (let V2500 (shen.lazyderef (tl V2499) V2919) (if (= () V2500) (do (shen.incinfs) (cut Throwcontrol V2919 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons (cons = (cons Action ())) (cons (cons fail ()) ())) ())) (cons Action ()))) V2917 V2918 V2919 V2920)))) false))) false)) false)) false)) (if (= Case false) (do (shen.incinfs) (shen.t* (cons V2916 (cons : (cons V2917 ()))) V2918 V2919 V2920)) Case)) Case)) Case)))))
 
-(defun shen.t*-pattern (V3013 V3014 V3015 V3016) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Hyp (shen.newpv V3015) (do (shen.incinfs) (shen.tms->hyp (shen.ues V3013) Hyp V3015 (freeze (cut Throwcontrol V3015 (freeze (shen.t* (cons V3013 (cons : (cons V3014 ()))) Hyp V3015 V3016))))))))))
+(defun shen.t*-pattern (V2921 V2922 V2923 V2924) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Hyp (shen.newpv V2923) (do (shen.incinfs) (shen.tms->hyp (shen.ues V2921) Hyp V2923 (freeze (cut Throwcontrol V2923 (freeze (shen.t* (cons V2921 (cons : (cons V2922 ()))) Hyp V2923 V2924))))))))))
 
-(defun shen.tms->hyp (V3017 V3018 V3019 V3020) (let Case (let V2549 (shen.lazyderef V3017 V3019) (if (= () V2549) (let V2550 (shen.lazyderef V3018 V3019) (if (= () V2550) (do (shen.incinfs) (thaw V3020)) (if (shen.pvar? V2550) (do (shen.bindv V2550 () V3019) (let Result (do (shen.incinfs) (thaw V3020)) (do (shen.unbindv V2550 V3019) Result))) false))) false)) (if (= Case false) (let V2551 (shen.lazyderef V3017 V3019) (if (cons? V2551) (let Tm2546 (hd V2551) (let Tms (tl V2551) (let V2552 (shen.lazyderef V3018 V3019) (if (cons? V2552) (let V2553 (shen.lazyderef (hd V2552) V3019) (if (cons? V2553) (let Tm (hd V2553) (let V2554 (shen.lazyderef (tl V2553) V3019) (if (cons? V2554) (let V2555 (shen.lazyderef (hd V2554) V3019) (if (= : V2555) (let V2556 (shen.lazyderef (tl V2554) V3019) (if (cons? V2556) (let A (hd V2556) (let V2557 (shen.lazyderef (tl V2556) V3019) (if (= () V2557) (let Hyp (tl V2552) (do (shen.incinfs) (unify! Tm Tm2546 V3019 (freeze (shen.tms->hyp Tms Hyp V3019 V3020))))) (if (shen.pvar? V2557) (do (shen.bindv V2557 () V3019) (let Result (let Hyp (tl V2552) (do (shen.incinfs) (unify! Tm Tm2546 V3019 (freeze (shen.tms->hyp Tms Hyp V3019 V3020))))) (do (shen.unbindv V2557 V3019) Result))) false)))) (if (shen.pvar? V2556) (let A (shen.newpv V3019) (do (shen.bindv V2556 (cons A ()) V3019) (let Result (let Hyp (tl V2552) (do (shen.incinfs) (unify! Tm Tm2546 V3019 (freeze (shen.tms->hyp Tms Hyp V3019 V3020))))) (do (shen.unbindv V2556 V3019) Result)))) false))) (if (shen.pvar? V2555) (do (shen.bindv V2555 : V3019) (let Result (let V2558 (shen.lazyderef (tl V2554) V3019) (if (cons? V2558) (let A (hd V2558) (let V2559 (shen.lazyderef (tl V2558) V3019) (if (= () V2559) (let Hyp (tl V2552) (do (shen.incinfs) (unify! Tm Tm2546 V3019 (freeze (shen.tms->hyp Tms Hyp V3019 V3020))))) (if (shen.pvar? V2559) (do (shen.bindv V2559 () V3019) (let Result (let Hyp (tl V2552) (do (shen.incinfs) (unify! Tm Tm2546 V3019 (freeze (shen.tms->hyp Tms Hyp V3019 V3020))))) (do (shen.unbindv V2559 V3019) Result))) false)))) (if (shen.pvar? V2558) (let A (shen.newpv V3019) (do (shen.bindv V2558 (cons A ()) V3019) (let Result (let Hyp (tl V2552) (do (shen.incinfs) (unify! Tm Tm2546 V3019 (freeze (shen.tms->hyp Tms Hyp V3019 V3020))))) (do (shen.unbindv V2558 V3019) Result)))) false))) (do (shen.unbindv V2555 V3019) Result))) false))) (if (shen.pvar? V2554) (let A (shen.newpv V3019) (do (shen.bindv V2554 (cons : (cons A ())) V3019) (let Result (let Hyp (tl V2552) (do (shen.incinfs) (unify! Tm Tm2546 V3019 (freeze (shen.tms->hyp Tms Hyp V3019 V3020))))) (do (shen.unbindv V2554 V3019) Result)))) false)))) (if (shen.pvar? V2553) (let Tm (shen.newpv V3019) (let A (shen.newpv V3019) (do (shen.bindv V2553 (cons Tm (cons : (cons A ()))) V3019) (let Result (let Hyp (tl V2552) (do (shen.incinfs) (unify! Tm Tm2546 V3019 (freeze (shen.tms->hyp Tms Hyp V3019 V3020))))) (do (shen.unbindv V2553 V3019) Result))))) false))) (if (shen.pvar? V2552) (let Tm (shen.newpv V3019) (let A (shen.newpv V3019) (let Hyp (shen.newpv V3019) (do (shen.bindv V2552 (cons (cons Tm (cons : (cons A ()))) Hyp) V3019) (let Result (do (shen.incinfs) (unify! Tm Tm2546 V3019 (freeze (shen.tms->hyp Tms Hyp V3019 V3020)))) (do (shen.unbindv V2552 V3019) Result)))))) false))))) false)) Case)))
+(defun shen.tms->hyp (V2925 V2926 V2927 V2928) (let Case (let V2465 (shen.lazyderef V2925 V2927) (if (= () V2465) (let V2466 (shen.lazyderef V2926 V2927) (if (= () V2466) (do (shen.incinfs) (thaw V2928)) (if (shen.pvar? V2466) (do (shen.bindv V2466 () V2927) (let Result (do (shen.incinfs) (thaw V2928)) (do (shen.unbindv V2466 V2927) Result))) false))) false)) (if (= Case false) (let V2467 (shen.lazyderef V2925 V2927) (if (cons? V2467) (let Tm2462 (hd V2467) (let Tms (tl V2467) (let V2468 (shen.lazyderef V2926 V2927) (if (cons? V2468) (let V2469 (shen.lazyderef (hd V2468) V2927) (if (cons? V2469) (let Tm (hd V2469) (let V2470 (shen.lazyderef (tl V2469) V2927) (if (cons? V2470) (let V2471 (shen.lazyderef (hd V2470) V2927) (if (= : V2471) (let V2472 (shen.lazyderef (tl V2470) V2927) (if (cons? V2472) (let A (hd V2472) (let V2473 (shen.lazyderef (tl V2472) V2927) (if (= () V2473) (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (if (shen.pvar? V2473) (do (shen.bindv V2473 () V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2473 V2927) Result))) false)))) (if (shen.pvar? V2472) (let A (shen.newpv V2927) (do (shen.bindv V2472 (cons A ()) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2472 V2927) Result)))) false))) (if (shen.pvar? V2471) (do (shen.bindv V2471 : V2927) (let Result (let V2474 (shen.lazyderef (tl V2470) V2927) (if (cons? V2474) (let A (hd V2474) (let V2475 (shen.lazyderef (tl V2474) V2927) (if (= () V2475) (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (if (shen.pvar? V2475) (do (shen.bindv V2475 () V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2475 V2927) Result))) false)))) (if (shen.pvar? V2474) (let A (shen.newpv V2927) (do (shen.bindv V2474 (cons A ()) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2474 V2927) Result)))) false))) (do (shen.unbindv V2471 V2927) Result))) false))) (if (shen.pvar? V2470) (let A (shen.newpv V2927) (do (shen.bindv V2470 (cons : (cons A ())) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2470 V2927) Result)))) false)))) (if (shen.pvar? V2469) (let Tm (shen.newpv V2927) (let A (shen.newpv V2927) (do (shen.bindv V2469 (cons Tm (cons : (cons A ()))) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2469 V2927) Result))))) false))) (if (shen.pvar? V2468) (let Tm (shen.newpv V2927) (let A (shen.newpv V2927) (let Hyp (shen.newpv V2927) (do (shen.bindv V2468 (cons (cons Tm (cons : (cons A ()))) Hyp) V2927) (let Result (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928)))) (do (shen.unbindv V2468 V2927) Result)))))) false))))) false)) Case)))
 
-(defun findall (V3021 V3022 V3023 V3024 V3025) (let B (shen.newpv V3024) (let A (shen.newpv V3024) (do (shen.incinfs) (bind A (gensym shen.a) V3024 (freeze (bind B (set (shen.lazyderef A V3024) ()) V3024 (freeze (shen.findallhelp V3021 V3022 V3023 A V3024 V3025)))))))))
+(defun findall (V2929 V2930 V2931 V2932 V2933) (let B (shen.newpv V2932) (let A (shen.newpv V2932) (do (shen.incinfs) (bind A (gensym shen.a) V2932 (freeze (bind B (set (shen.lazyderef A V2932) ()) V2932 (freeze (shen.findallhelp V2929 V2930 V2931 A V2932 V2933)))))))))
 
-(defun shen.findallhelp (V3026 V3027 V3028 V3029 V3030 V3031) (let Case (do (shen.incinfs) (call V3027 V3030 (freeze (shen.remember V3029 V3026 V3030 (freeze (fwhen false V3030 V3031)))))) (if (= Case false) (do (shen.incinfs) (bind V3028 (value (shen.lazyderef V3029 V3030)) V3030 V3031)) Case)))
+(defun shen.findallhelp (V2934 V2935 V2936 V2937 V2938 V2939) (let Case (do (shen.incinfs) (call V2935 V2938 (freeze (shen.remember V2937 V2934 V2938 (freeze (fwhen false V2938 V2939)))))) (if (= Case false) (do (shen.incinfs) (bind V2936 (value (shen.lazyderef V2937 V2938)) V2938 V2939)) Case)))
 
-(defun shen.remember (V3032 V3033 V3034 V3035) (let B (shen.newpv V3034) (do (shen.incinfs) (bind B (set (shen.deref V3032 V3034) (cons (shen.deref V3033 V3034) (value (shen.deref V3032 V3034)))) V3034 V3035))))
-
-(defun shen.t*-defcc (V3036 V3037 V3038 V3039 V3040) (let V2522 (shen.lazyderef V3036 V3039) (if (cons? V2522) (let V2523 (shen.lazyderef (hd V2522) V3039) (if (= defcc V2523) (let V2524 (shen.lazyderef (tl V2522) V3039) (if (cons? V2524) (let F (hd V2524) (let V2525 (shen.lazyderef (tl V2524) V3039) (if (cons? V2525) (let V2526 (shen.lazyderef (hd V2525) V3039) (if (= { V2526) (let V2527 (shen.lazyderef (tl V2525) V3039) (if (cons? V2527) (let V2528 (shen.lazyderef (hd V2527) V3039) (if (cons? V2528) (let V2529 (shen.lazyderef (hd V2528) V3039) (if (= list V2529) (let V2530 (shen.lazyderef (tl V2528) V3039) (if (cons? V2530) (let A (hd V2530) (let V2531 (shen.lazyderef (tl V2530) V3039) (if (= () V2531) (let V2532 (shen.lazyderef (tl V2527) V3039) (if (cons? V2532) (let V2533 (shen.lazyderef (hd V2532) V3039) (if (= ==> V2533) (let V2534 (shen.lazyderef (tl V2532) V3039) (if (cons? V2534) (let B (hd V2534) (let V2535 (shen.lazyderef (tl V2534) V3039) (if (cons? V2535) (let V2536 (shen.lazyderef (hd V2535) V3039) (if (= } V2536) (let Rest (tl V2535) (do (shen.incinfs) (shen.t*-defcc-h (cons defcc (cons F (cons (shen.ue (shen.demodulate (cons (cons list (cons A ())) (cons ==> (cons B ()))))) (shen.ue (shen.split_cc_rules false (shen.plug-wildcards Rest) ()))))) V3037 V3038 V3039 V3040))) false)) false))) false)) false)) false)) false))) false)) false)) false)) false)) false)) false))) false)) false)) false)))
-
-(defun shen.plug-wildcards (V3041) (cond ((cons? V3041) (map (lambda X2881 (shen.plug-wildcards X2881)) V3041)) ((= V3041 _) (gensym (intern "X"))) (true V3041)))
-
-(defun shen.t*-defcc-h (V3042 V3043 V3044 V3045 V3046) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let V2506 (shen.lazyderef V3042 V3045) (if (cons? V2506) (let V2507 (shen.lazyderef (hd V2506) V3045) (if (= defcc V2507) (let V2508 (shen.lazyderef (tl V2506) V3045) (if (cons? V2508) (let F (hd V2508) (let V2509 (shen.lazyderef (tl V2508) V3045) (if (cons? V2509) (let V2510 (shen.lazyderef (hd V2509) V3045) (if (cons? V2510) (let V2511 (shen.lazyderef (hd V2510) V3045) (if (cons? V2511) (let V2512 (shen.lazyderef (hd V2511) V3045) (if (= list V2512) (let V2513 (shen.lazyderef (tl V2511) V3045) (if (cons? V2513) (let A (hd V2513) (let V2514 (shen.lazyderef (tl V2513) V3045) (if (= () V2514) (let V2515 (shen.lazyderef (tl V2510) V3045) (if (cons? V2515) (let V2516 (shen.lazyderef (hd V2515) V3045) (if (= ==> V2516) (let V2517 (shen.lazyderef (tl V2515) V3045) (if (cons? V2517) (let B (hd V2517) (let V2518 (shen.lazyderef (tl V2517) V3045) (if (= () V2518) (let Rules (tl V2509) (let Declare (shen.newpv V3045) (do (shen.incinfs) (cut Throwcontrol V3045 (freeze (shen.tc-rules F Rules (cons list (cons A ())) B (cons (cons F (cons : (cons (cons (cons list (cons A ())) (cons ==> (cons B ()))) ()))) V3044) 1 V3045 (freeze (unify V3043 (cons (cons list (cons A ())) (cons ==> (cons B ()))) V3045 (freeze (bind Declare (declare (shen.lazyderef F V3045) (cons (cons list (cons (shen.lazyderef A V3045) ())) (cons ==> (cons (shen.lazyderef B V3045) ())))) V3045 V3046)))))))))) false))) false)) false)) false)) false))) false)) false)) false)) false)) false))) false)) false)) false)))))
-
-(defun shen.tc-rules (V3047 V3048 V3049 V3050 V3051 V3052 V3053 V3054) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2497 (shen.lazyderef V3048 V3053) (if (= () V2497) (do (shen.incinfs) (thaw V3054)) false)) (if (= Case false) (let V2498 (shen.lazyderef V3048 V3053) (if (cons? V2498) (let Rule (hd V2498) (let Rules (tl V2498) (let V2499 (shen.lazyderef V3049 V3053) (if (cons? V2499) (let V2500 (shen.lazyderef (hd V2499) V3053) (if (= list V2500) (let V2501 (shen.lazyderef (tl V2499) V3053) (if (cons? V2501) (let A (hd V2501) (let V2502 (shen.lazyderef (tl V2501) V3053) (if (= () V2502) (let M (shen.newpv V3053) (do (shen.incinfs) (shen.tc-rule V3047 Rule A V3050 V3051 V3052 V3053 (freeze (bind M (+ (shen.deref V3052 V3053) 1) V3053 (freeze (cut Throwcontrol V3053 (freeze (shen.tc-rules V3047 Rules (cons list (cons A ())) V3050 V3051 M V3053 V3054))))))))) false))) false)) false)) false)))) false)) Case)))))
-
-(defun shen.tc-rule (V3055 V3056 V3057 V3058 V3059 V3060 V3061 V3062) (let Case (do (shen.incinfs) (shen.check-defcc-rule V3056 V3057 V3058 V3059 V3061 V3062)) (if (= Case false) (let Err (shen.newpv V3061) (do (shen.incinfs) (bind Err (simple-error (cn "type error in rule " (shen.app (shen.lazyderef V3060 V3061) (cn " of " (shen.app (shen.lazyderef V3055 V3061) "" shen.a)) shen.a))) V3061 V3062))) Case)))
-
-(defun shen.check-defcc-rule (V3063 V3064 V3065 V3066 V3067 V3068) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let V2482 (shen.lazyderef V3063 V3067) (if (cons? V2482) (let Syntax (hd V2482) (let V2483 (shen.lazyderef (tl V2482) V3067) (if (cons? V2483) (let Semantics (hd V2483) (let V2484 (shen.lazyderef (tl V2483) V3067) (if (= () V2484) (let SynHyps (shen.newpv V3067) (do (shen.incinfs) (shen.syntax-hyps Syntax V3066 SynHyps V3064 V3067 (freeze (cut Throwcontrol V3067 (freeze (shen.syntax-check Syntax V3064 SynHyps V3067 (freeze (cut Throwcontrol V3067 (freeze (shen.semantics-check Semantics V3065 SynHyps V3067 V3068))))))))))) false))) false))) false)))))
-
-(defun shen.syntax-hyps (V3069 V3070 V3071 V3072 V3073 V3074) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2467 (shen.lazyderef V3069 V3073) (if (= () V2467) (do (shen.incinfs) (unify! V3071 V3070 V3073 V3074)) false)) (if (= Case false) (let Case (let V2468 (shen.lazyderef V3069 V3073) (if (cons? V2468) (let X2461 (hd V2468) (let Y (tl V2468) (let V2469 (shen.lazyderef V3071 V3073) (if (cons? V2469) (let V2470 (shen.lazyderef (hd V2469) V3073) (if (cons? V2470) (let X (hd V2470) (let V2471 (shen.lazyderef (tl V2470) V3073) (if (cons? V2471) (let V2472 (shen.lazyderef (hd V2471) V3073) (if (= : V2472) (let V2473 (shen.lazyderef (tl V2471) V3073) (if (cons? V2473) (let A2462 (hd V2473) (let V2474 (shen.lazyderef (tl V2473) V3073) (if (= () V2474) (let SynHyps (tl V2469) (do (shen.incinfs) (unify! V3072 A2462 V3073 (freeze (unify! X X2461 V3073 (freeze (fwhen (shen.ue? (shen.deref X V3073)) V3073 (freeze (cut Throwcontrol V3073 (freeze (shen.syntax-hyps Y V3070 SynHyps V3072 V3073 V3074))))))))))) (if (shen.pvar? V2474) (do (shen.bindv V2474 () V3073) (let Result (let SynHyps (tl V2469) (do (shen.incinfs) (unify! V3072 A2462 V3073 (freeze (unify! X X2461 V3073 (freeze (fwhen (shen.ue? (shen.deref X V3073)) V3073 (freeze (cut Throwcontrol V3073 (freeze (shen.syntax-hyps Y V3070 SynHyps V3072 V3073 V3074))))))))))) (do (shen.unbindv V2474 V3073) Result))) false)))) (if (shen.pvar? V2473) (let A2462 (shen.newpv V3073) (do (shen.bindv V2473 (cons A2462 ()) V3073) (let Result (let SynHyps (tl V2469) (do (shen.incinfs) (unify! V3072 A2462 V3073 (freeze (unify! X X2461 V3073 (freeze (fwhen (shen.ue? (shen.deref X V3073)) V3073 (freeze (cut Throwcontrol V3073 (freeze (shen.syntax-hyps Y V3070 SynHyps V3072 V3073 V3074))))))))))) (do (shen.unbindv V2473 V3073) Result)))) false))) (if (shen.pvar? V2472) (do (shen.bindv V2472 : V3073) (let Result (let V2475 (shen.lazyderef (tl V2471) V3073) (if (cons? V2475) (let A2462 (hd V2475) (let V2476 (shen.lazyderef (tl V2475) V3073) (if (= () V2476) (let SynHyps (tl V2469) (do (shen.incinfs) (unify! V3072 A2462 V3073 (freeze (unify! X X2461 V3073 (freeze (fwhen (shen.ue? (shen.deref X V3073)) V3073 (freeze (cut Throwcontrol V3073 (freeze (shen.syntax-hyps Y V3070 SynHyps V3072 V3073 V3074))))))))))) (if (shen.pvar? V2476) (do (shen.bindv V2476 () V3073) (let Result (let SynHyps (tl V2469) (do (shen.incinfs) (unify! V3072 A2462 V3073 (freeze (unify! X X2461 V3073 (freeze (fwhen (shen.ue? (shen.deref X V3073)) V3073 (freeze (cut Throwcontrol V3073 (freeze (shen.syntax-hyps Y V3070 SynHyps V3072 V3073 V3074))))))))))) (do (shen.unbindv V2476 V3073) Result))) false)))) (if (shen.pvar? V2475) (let A2462 (shen.newpv V3073) (do (shen.bindv V2475 (cons A2462 ()) V3073) (let Result (let SynHyps (tl V2469) (do (shen.incinfs) (unify! V3072 A2462 V3073 (freeze (unify! X X2461 V3073 (freeze (fwhen (shen.ue? (shen.deref X V3073)) V3073 (freeze (cut Throwcontrol V3073 (freeze (shen.syntax-hyps Y V3070 SynHyps V3072 V3073 V3074))))))))))) (do (shen.unbindv V2475 V3073) Result)))) false))) (do (shen.unbindv V2472 V3073) Result))) false))) (if (shen.pvar? V2471) (let A2462 (shen.newpv V3073) (do (shen.bindv V2471 (cons : (cons A2462 ())) V3073) (let Result (let SynHyps (tl V2469) (do (shen.incinfs) (unify! V3072 A2462 V3073 (freeze (unify! X X2461 V3073 (freeze (fwhen (shen.ue? (shen.deref X V3073)) V3073 (freeze (cut Throwcontrol V3073 (freeze (shen.syntax-hyps Y V3070 SynHyps V3072 V3073 V3074))))))))))) (do (shen.unbindv V2471 V3073) Result)))) false)))) (if (shen.pvar? V2470) (let X (shen.newpv V3073) (let A2462 (shen.newpv V3073) (do (shen.bindv V2470 (cons X (cons : (cons A2462 ()))) V3073) (let Result (let SynHyps (tl V2469) (do (shen.incinfs) (unify! V3072 A2462 V3073 (freeze (unify! X X2461 V3073 (freeze (fwhen (shen.ue? (shen.deref X V3073)) V3073 (freeze (cut Throwcontrol V3073 (freeze (shen.syntax-hyps Y V3070 SynHyps V3072 V3073 V3074))))))))))) (do (shen.unbindv V2470 V3073) Result))))) false))) (if (shen.pvar? V2469) (let X (shen.newpv V3073) (let A2462 (shen.newpv V3073) (let SynHyps (shen.newpv V3073) (do (shen.bindv V2469 (cons (cons X (cons : (cons A2462 ()))) SynHyps) V3073) (let Result (do (shen.incinfs) (unify! V3072 A2462 V3073 (freeze (unify! X X2461 V3073 (freeze (fwhen (shen.ue? (shen.deref X V3073)) V3073 (freeze (cut Throwcontrol V3073 (freeze (shen.syntax-hyps Y V3070 SynHyps V3072 V3073 V3074)))))))))) (do (shen.unbindv V2469 V3073) Result)))))) false))))) false)) (if (= Case false) (let V2477 (shen.lazyderef V3069 V3073) (if (cons? V2477) (let Y (tl V2477) (do (shen.incinfs) (shen.syntax-hyps Y V3070 V3071 V3072 V3073 V3074))) false)) Case)) Case)))))
-
-(defun shen.syntax-check (V3075 V3076 V3077 V3078 V3079) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2457 (shen.lazyderef V3075 V3078) (if (= () V2457) (do (shen.incinfs) (thaw V3079)) false)) (if (= Case false) (let Case (let V2458 (shen.lazyderef V3075 V3078) (if (cons? V2458) (let X (hd V2458) (let Syntax (tl V2458) (let C (shen.newpv V3078) (do (shen.incinfs) (fwhen (shen.grammar_symbol? (shen.lazyderef X V3078)) V3078 (freeze (cut Throwcontrol V3078 (freeze (shen.t* (cons X (cons : (cons (cons (cons list (cons V3076 ())) (cons ==> (cons C ()))) ()))) V3077 V3078 (freeze (cut Throwcontrol V3078 (freeze (shen.syntax-check Syntax V3076 V3077 V3078 V3079))))))))))))) false)) (if (= Case false) (let V2459 (shen.lazyderef V3075 V3078) (if (cons? V2459) (let X (hd V2459) (let Syntax (tl V2459) (do (shen.incinfs) (shen.t* (cons X (cons : (cons V3076 ()))) V3077 V3078 (freeze (cut Throwcontrol V3078 (freeze (shen.syntax-check Syntax V3076 V3077 V3078 V3079)))))))) false)) Case)) Case)))))
-
-(defun shen.semantics-check (V3080 V3081 V3082 V3083 V3084) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2449 (shen.lazyderef V3080 V3083) (if (cons? V2449) (let V2450 (shen.lazyderef (hd V2449) V3083) (if (= where V2450) (let V2451 (shen.lazyderef (tl V2449) V3083) (if (cons? V2451) (let P (hd V2451) (let V2452 (shen.lazyderef (tl V2451) V3083) (if (cons? V2452) (let Q (hd V2452) (let V2453 (shen.lazyderef (tl V2452) V3083) (if (= () V2453) (do (shen.incinfs) (cut Throwcontrol V3083 (freeze (shen.t* (cons (shen.curry P) (cons : (cons boolean ()))) V3082 V3083 (freeze (shen.t* (cons (shen.curry Q) (cons : (cons V3081 ()))) V3082 V3083 V3084)))))) false))) false))) false)) false)) false)) (if (= Case false) (let Semantics* (shen.newpv V3083) (do (shen.incinfs) (bind Semantics* (shen.curry (shen.rename-semantics (shen.deref V3080 V3083))) V3083 (freeze (shen.t* (cons Semantics* (cons : (cons V3081 ()))) V3082 V3083 V3084))))) Case)))))
-
-(defun shen.rename-semantics (V3085) (cond ((cons? V3085) (cons (shen.rename-semantics (hd V3085)) (shen.rename-semantics (tl V3085)))) ((shen.grammar_symbol? V3085) (cons shen.<-sem (cons V3085 ()))) (true V3085)))
-
-"(defprolog syntax-check
-  (mode [] -) _ _ <--;
-  (mode [X | Syntax] -) A Hyps <-- (fwhen (grammar_symbol? X))
-                                   !
-                                   (t* [X : [[list B] ==> C]] Hyps)
-                                   !
-                                   (bind X&& (concat && X))
-                                   !
-                                   (t* [X&& : [list A]] [[X&& : [list B]] | Hyps]) 
-                                   !
-                                   (syntax-check Syntax A Hyps);
-  (mode [X | Syntax] -) A Hyps <-- (t* [X : A] Hyps)
-                                   !
-                                   (syntax-check Syntax A Hyps);)"
+(defun shen.remember (V2940 V2941 V2942 V2943) (let B (shen.newpv V2942) (do (shen.incinfs) (bind B (set (shen.deref V2940 V2942) (cons (shen.deref V2941 V2942) (value (shen.deref V2940 V2942)))) V2942 V2943))))