diff options
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 204 |
1 files changed, 102 insertions, 102 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index 2e3cb041..03d5fcf5 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,6 +1,6 @@ -(142449 . 3409757251) -(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) #0#) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(142449 . 3409760523) +(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) #0#) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) (((|#2| |#2|) . T)) ((((-520)) . T)) ((($ $) -3700 (|has| |#2| (-157)) (|has| |#2| (-336)) (|has| |#2| (-424)) (|has| |#2| (-512)) (|has| |#2| (-837))) ((|#2| |#2|) . T) ((#0=(-380 (-520)) #0#) |has| |#2| (-37 (-380 (-520))))) @@ -41,10 +41,10 @@ (((|#1|) . T) (((-520)) |has| |#1| (-960 (-520))) (((-380 (-520))) |has| |#1| (-960 (-380 (-520))))) (-3700 (|has| |#2| (-157)) (|has| |#2| (-424)) (|has| |#2| (-512)) (|has| |#2| (-837))) (-3700 (|has| |#1| (-157)) (|has| |#1| (-424)) (|has| |#1| (-512)) (|has| |#1| (-837))) -(((|#2| (-453 (-3479 |#1|) (-706))) . T)) +(((|#2| (-453 (-3474 |#1|) (-706))) . T)) (((|#1| (-492 (-1083))) . T)) (((#0=(-798 |#1|) #0#) . T) ((#1=(-380 (-520)) #1#) . T) (($ $) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (|has| |#4| (-341)) (|has| |#3| (-341)) (((|#1|) . T)) @@ -92,7 +92,7 @@ ((($) . T)) (|has| |#1| (-341)) (((|#1|) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) ((((-791)) . T)) ((((-791)) . T)) @@ -202,8 +202,8 @@ (((|#1|) . T)) ((((-380 (-520))) |has| |#1| (-960 (-380 (-520)))) (((-520)) |has| |#1| (-960 (-520))) ((|#1|) . T)) (((|#1|) . T) (((-520)) |has| |#1| (-582 (-520)))) -(((|#2|) . T) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) (|has| |#1| (-512)) (|has| |#1| (-512)) (((|#1| |#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) @@ -238,7 +238,7 @@ (((|#1|) . T) (((-520)) |has| |#1| (-960 (-520))) (((-380 (-520))) |has| |#1| (-960 (-380 (-520))))) ((($) . T) (((-380 (-520))) |has| |#2| (-37 (-380 (-520)))) ((|#2|) . T)) ((((-380 $) (-380 $)) |has| |#2| (-512)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 (-51)))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 (-51)))) . T)) (((|#1|) . T)) (|has| |#2| (-837)) ((((-1066) (-51)) . T)) @@ -271,7 +271,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1059)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) (|has| (-1150 |#1| |#2| |#3| |#4|) (-133)) (|has| (-1150 |#1| |#2| |#3| |#4|) (-135)) (|has| |#1| (-133)) @@ -288,9 +288,9 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-969))) ((((-791)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) #0#) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) #0#) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) (((|#1|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012))) ((#0=(-2 (|:| -2534 (-1066)) (|:| -3049 |#1|)) #0#) |has| (-2 (|:| -2534 (-1066)) (|:| -3049 |#1|)) (-283 (-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012))) ((#0=(-2 (|:| -2526 (-1066)) (|:| -3043 |#1|)) #0#) |has| (-2 (|:| -2526 (-1066)) (|:| -3043 |#1|)) (-283 (-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))))) ((((-520) |#1|) . T)) ((((-791)) . T)) ((((-496)) -12 (|has| |#1| (-561 (-496))) (|has| |#2| (-561 (-496)))) (((-820 (-352))) -12 (|has| |#1| (-561 (-820 (-352)))) (|has| |#2| (-561 (-820 (-352))))) (((-820 (-520))) -12 (|has| |#1| (-561 (-820 (-520)))) (|has| |#2| (-561 (-820 (-520)))))) @@ -381,11 +381,11 @@ ((((-132)) . T)) (((|#3|) |has| |#3| (-1012)) (((-520)) -12 (|has| |#3| (-960 (-520))) (|has| |#3| (-1012))) (((-380 (-520))) -12 (|has| |#3| (-960 (-380 (-520)))) (|has| |#3| (-1012)))) ((((-791)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#1|) . T)) ((((-791)) -3700 (|has| |#1| (-560 (-791))) (|has| |#1| (-783)) (|has| |#1| (-1012)))) ((((-496)) |has| |#1| (-561 (-496)))) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) . T)) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) . T)) (|has| |#1| (-336)) (-3700 (|has| |#1| (-21)) (|has| |#1| (-781))) ((((-1083) |#1|) |has| |#1| (-481 (-1083) |#1|)) ((|#1| |#1|) |has| |#1| (-283 |#1|))) @@ -394,13 +394,13 @@ (|has| |#1| (-781)) (-3700 (|has| |#1| (-783)) (|has| |#1| (-1012))) ((((-791)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-496)) |has| |#1| (-561 (-496)))) (((|#1| |#2|) . T)) ((((-1083)) -12 (|has| |#1| (-336)) (|has| |#1| (-828 (-1083))))) ((((-1066) |#1|) . T)) (((|#1| |#2| |#3| (-492 |#3|)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (|has| |#1| (-341)) (|has| |#1| (-341)) (|has| |#1| (-341)) @@ -583,7 +583,7 @@ (((|#4| |#4|) -12 (|has| |#4| (-283 |#4|)) (|has| |#4| (-1012)))) (((|#2|) . T) (((-520)) |has| |#2| (-960 (-520))) (((-380 (-520))) |has| |#2| (-960 (-380 (-520))))) (((|#3| |#3|) -12 (|has| |#3| (-283 |#3|)) (|has| |#3| (-1012)))) -(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) @@ -591,7 +591,7 @@ (((|#2|) . T)) (((|#3|) . T)) (-3700 (|has| |#1| (-783)) (|has| |#1| (-1012))) -(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) (((|#2|) . T)) ((((-791)) -3700 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-560 (-791))) (|has| |#2| (-157)) (|has| |#2| (-336)) (|has| |#2| (-341)) (|has| |#2| (-728)) (|has| |#2| (-781)) (|has| |#2| (-969)) (|has| |#2| (-1012))) (((-1164 |#2|)) . T)) (((|#1|) |has| |#1| (-157))) @@ -663,9 +663,9 @@ (-3700 (|has| |#1| (-424)) (|has| |#1| (-837))) ((((-520) |#2|) . T)) ((((-791)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) ((($) -3700 (|has| |#3| (-157)) (|has| |#3| (-781)) (|has| |#3| (-969))) ((|#3|) -3700 (|has| |#3| (-157)) (|has| |#3| (-336)) (|has| |#3| (-969)))) ((((-520) |#1|) . T)) @@ -680,11 +680,11 @@ (|has| |#1| (-512)) (|has| |#1| (-37 (-380 (-520)))) (|has| |#1| (-37 (-380 (-520)))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-791)) . T)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) (|has| |#1| (-37 (-380 (-520)))) -((((-361) (-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) +((((-361) (-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) (|has| |#1| (-37 (-380 (-520)))) (|has| |#2| (-1059)) (-3700 (|has| |#1| (-336)) (|has| |#1| (-512))) @@ -855,7 +855,7 @@ (|has| |#1| (-135)) (|has| |#1| (-133)) (|has| |#4| (-781)) -(((|#2| (-216 (-3479 |#1|) (-706)) (-793 |#1|)) . T)) +(((|#2| (-216 (-3474 |#1|) (-706)) (-793 |#1|)) . T)) (|has| |#3| (-781)) (((|#1| (-492 |#3|) |#3|) . T)) (|has| |#1| (-135)) @@ -875,7 +875,7 @@ (|has| |#2| (-157)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-209)) (|has| |#2| (-969))) -(((|#2|) . T) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (-3700 (|has| |#3| (-728)) (|has| |#3| (-781))) (-3700 (|has| |#3| (-728)) (|has| |#3| (-781))) ((((-791)) . T)) @@ -905,10 +905,10 @@ (((|#1| (-380 (-520))) . T)) (((|#3|) . T) (((-559 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((($ $) . T) ((|#2| $) . T)) (((|#1|) . T) (((-380 (-520))) . T) (($) . T)) (((#0=(-1081 |#1| |#2| |#3|) #0#) -12 (|has| (-1081 |#1| |#2| |#3|) (-283 (-1081 |#1| |#2| |#3|))) (|has| |#1| (-336))) (((-1083) #0#) -12 (|has| (-1081 |#1| |#2| |#3|) (-481 (-1083) (-1081 |#1| |#2| |#3|))) (|has| |#1| (-336)))) @@ -916,8 +916,8 @@ ((((-791)) . T)) ((((-791)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) -(((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012))) (((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) |has| (-2 (|:| -2534 (-1066)) (|:| -3049 |#1|)) (-283 (-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))))) +(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) +(((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012))) (((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) |has| (-2 (|:| -2526 (-1066)) (|:| -3043 |#1|)) (-283 (-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))))) ((((-791)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -930,7 +930,7 @@ (|has| |#1| (-1012)) (((|#2| |#2|) -3700 (|has| |#2| (-157)) (|has| |#2| (-336)) (|has| |#2| (-969))) (($ $) |has| |#2| (-157))) (((|#2|) -3700 (|has| |#2| (-157)) (|has| |#2| (-336)))) -((((-520) (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T) ((|#1| |#2|) . T)) +((((-520) (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T) ((|#1| |#2|) . T)) (((|#2|) -3700 (|has| |#2| (-157)) (|has| |#2| (-336)) (|has| |#2| (-969))) (($) |has| |#2| (-157))) ((((-706)) . T)) ((((-520)) . T)) @@ -960,7 +960,7 @@ (-3700 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-336)) (|has| |#2| (-341)) (|has| |#2| (-728)) (|has| |#2| (-781)) (|has| |#2| (-969)) (|has| |#2| (-1012))) (-12 (|has| |#3| (-209)) (|has| |#3| (-969))) (|has| |#2| (-1059)) -(((#0=(-51)) . T) (((-2 (|:| -2534 (-1083)) (|:| -3049 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -2526 (-1083)) (|:| -3043 #0#))) . T)) (((|#1| |#2|) . T)) (-3700 (|has| |#3| (-157)) (|has| |#3| (-781)) (|has| |#3| (-969))) (((|#1| (-520) (-997)) . T)) @@ -985,7 +985,7 @@ ((((-791)) . T)) (|has| |#1| (-322)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) #0#) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) #0#) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) (|has| |#1| (-512)) (((|#1| |#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) ((((-791)) . T)) @@ -1036,7 +1036,7 @@ (-12 (|has| |#1| (-728)) (|has| |#2| (-728))) (-3700 (|has| |#2| (-157)) (|has| |#2| (-781)) (|has| |#2| (-969))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (|has| |#1| (-1104)) (((#0=(-520) #0#) . T) ((#1=(-380 (-520)) #1#) . T) (($ $) . T)) ((((-380 (-520))) . T) (($) . T)) @@ -1065,7 +1065,7 @@ (|has| |#1| (-781)) ((($) . T) (((-380 (-520))) -3700 (|has| |#1| (-336)) (|has| |#1| (-322))) ((|#1|) . T)) (-3700 (|has| |#1| (-157)) (|has| |#1| (-512))) -(((#0=(-2 (|:| -2534 (-1083)) (|:| -3049 (-51))) #0#) |has| (-2 (|:| -2534 (-1083)) (|:| -3049 (-51))) (-283 (-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))))) +(((#0=(-2 (|:| -2526 (-1083)) (|:| -3043 (-51))) #0#) |has| (-2 (|:| -2526 (-1083)) (|:| -3043 (-51))) (-283 (-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))))) ((($) . T)) (|has| |#2| (-783)) ((($) . T)) @@ -1078,10 +1078,10 @@ ((((-791)) . T)) ((((-520)) |has| #0=(-380 |#2|) (-582 (-520))) ((#0#) . T)) ((((-520) (-132)) . T)) -((((-520) (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T) ((|#1| |#2|) . T)) +((((-520) (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T) ((|#1| |#2|) . T)) ((((-380 (-520))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-791)) . T)) ((((-838 |#1|)) . T)) (|has| |#1| (-336)) @@ -1106,7 +1106,7 @@ ((($) . T)) (((|#2|) . T) (($) . T)) (((|#1|) |has| |#1| (-157))) -((((-520) (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T) ((|#1| |#2|) . T)) +((((-520) (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) ((($) |has| |#1| (-512)) ((|#1|) |has| |#1| (-157)) (((-380 (-520))) |has| |#1| (-37 (-380 (-520))))) (((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) @@ -1118,7 +1118,7 @@ (((|#1|) . T)) ((((-496)) |has| |#1| (-561 (-496))) (((-820 (-352))) |has| |#1| (-561 (-820 (-352)))) (((-820 (-520))) |has| |#1| (-561 (-820 (-520))))) ((((-791)) . T)) -(((|#2|) . T) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (|has| |#2| (-781)) (-12 (|has| |#2| (-209)) (|has| |#2| (-969))) (|has| |#1| (-512)) @@ -1143,7 +1143,7 @@ (((|#1|) . T)) (((|#2|) . T)) ((((-1083)) |has| (-380 |#2|) (-828 (-1083)))) -(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) #0#) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) #0#) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) @@ -1153,7 +1153,7 @@ (((|#2| |#2|) -3700 (|has| |#2| (-157)) (|has| |#2| (-336)) (|has| |#2| (-969))) (($ $) |has| |#2| (-157))) ((((-791)) . T)) ((((-791)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T) ((|#2|) . T)) ((((-791)) . T)) ((((-791)) . T)) ((((-1066) (-1083) (-520) (-201) (-791)) . T)) @@ -1235,7 +1235,7 @@ ((((-923 |#1|)) . T) ((|#1|) . T)) ((((-791)) . T)) ((((-791)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-380 (-520))) . T) (((-380 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1079 |#1|)) . T)) ((((-520)) . T) (($) . T) (((-380 (-520))) . T)) @@ -1243,7 +1243,7 @@ (|has| |#1| (-783)) (((|#2|) . T)) ((((-520)) . T) (($) . T) (((-380 (-520))) . T)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) ((((-520) |#2|) . T)) ((((-791)) -3700 (|has| |#1| (-560 (-791))) (|has| |#1| (-1012)))) (((|#2|) . T)) @@ -1260,7 +1260,7 @@ (((|#3|) -12 (|has| |#3| (-283 |#3|)) (|has| |#3| (-1012)))) (((|#2|) . T)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) #0#) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) #0#) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) (((|#2| |#2|) . T)) (|has| |#2| (-336)) (((|#2|) . T) (((-520)) |has| |#2| (-960 (-520))) (((-380 (-520))) |has| |#2| (-960 (-380 (-520))))) @@ -1290,7 +1290,7 @@ (((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) (((|#1| |#2|) . T)) ((((-520) (-132)) . T)) -(((#0=(-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) #0#) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012)))) +(((#0=(-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) #0#) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012)))) ((($) -3700 (|has| |#1| (-424)) (|has| |#1| (-512)) (|has| |#1| (-837))) ((|#1|) |has| |#1| (-157)) (((-380 (-520))) |has| |#1| (-37 (-380 (-520))))) (|has| |#1| (-783)) (((|#2| (-706) (-997)) . T)) @@ -1332,7 +1332,7 @@ ((((-361) (-1066)) . T)) ((($) |has| |#1| (-512)) ((|#1|) |has| |#1| (-157)) (((-380 (-520))) |has| |#1| (-37 (-380 (-520))))) ((((-791)) -3700 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-560 (-791))) (|has| |#2| (-157)) (|has| |#2| (-336)) (|has| |#2| (-341)) (|has| |#2| (-728)) (|has| |#2| (-781)) (|has| |#2| (-969)) (|has| |#2| (-1012))) (((-1164 |#2|)) . T)) -(((#0=(-51)) . T) (((-2 (|:| -2534 (-1066)) (|:| -3049 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -2526 (-1066)) (|:| -3043 #0#))) . T)) (((|#1|) . T)) ((((-791)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012)))) @@ -1358,7 +1358,7 @@ ((((-791)) . T)) ((((-791)) . T)) (|has| |#1| (-1012)) -(((|#2| (-453 (-3479 |#1|) (-706)) (-793 |#1|)) . T)) +(((|#2| (-453 (-3474 |#1|) (-706)) (-793 |#1|)) . T)) ((((-380 (-520))) . #0=(|has| |#2| (-336))) (($) . #0#)) (((|#1| (-492 (-1083)) (-1083)) . T)) (((|#1|) . T)) @@ -1378,11 +1378,11 @@ (|has| |#1| (-135)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) . T)) +(((|#1|) . T) (((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) . T)) ((((-1081 |#1| |#2| |#3|)) |has| |#1| (-336))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-1083) (-51)) . T)) ((($ $) . T)) (((|#1| (-520)) . T)) @@ -1427,11 +1427,11 @@ (|has| |#1| (-37 (-380 (-520)))) (-3700 (|has| |#1| (-336)) (|has| |#1| (-322))) (|has| |#1| (-37 (-380 (-520)))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-1083)) |has| |#1| (-828 (-1083))) (((-997)) . T)) (((|#1|) . T)) (|has| |#1| (-781)) -(((#0=(-2 (|:| -2534 (-1066)) (|:| -3049 (-51))) #0#) |has| (-2 (|:| -2534 (-1066)) (|:| -3049 (-51))) (-283 (-2 (|:| -2534 (-1066)) (|:| -3049 (-51)))))) +(((#0=(-2 (|:| -2526 (-1066)) (|:| -3043 (-51))) #0#) |has| (-2 (|:| -2526 (-1066)) (|:| -3043 (-51))) (-283 (-2 (|:| -2526 (-1066)) (|:| -3043 (-51)))))) (((|#1| |#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) (|has| |#1| (-1012)) (((|#1|) . T)) @@ -1470,7 +1470,7 @@ (((|#1| |#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012))) ((#0=(-2 (|:| -2534 (-1066)) (|:| -3049 |#1|)) #0#) |has| (-2 (|:| -2534 (-1066)) (|:| -3049 |#1|)) (-283 (-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012))) ((#0=(-2 (|:| -2526 (-1066)) (|:| -3043 |#1|)) #0#) |has| (-2 (|:| -2526 (-1066)) (|:| -3043 |#1|)) (-283 (-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))))) (-3700 (|has| |#2| (-424)) (|has| |#2| (-837))) (-3700 (|has| |#1| (-424)) (|has| |#1| (-837))) (((|#1|) . T) (($) . T)) @@ -1496,7 +1496,7 @@ ((((-380 (-520))) -3700 (|has| |#1| (-37 (-380 (-520)))) (|has| |#1| (-336))) (($) -3700 (|has| |#1| (-336)) (|has| |#1| (-512))) (((-1081 |#1| |#2| |#3|)) |has| |#1| (-336)) ((|#1|) |has| |#1| (-157))) (((|#1|) |has| |#1| (-157)) (((-380 (-520))) -3700 (|has| |#1| (-37 (-380 (-520)))) (|has| |#1| (-336))) (($) -3700 (|has| |#1| (-336)) (|has| |#1| (-512)))) ((($) |has| |#1| (-512)) ((|#1|) |has| |#1| (-157)) (((-380 (-520))) |has| |#1| (-37 (-380 (-520))))) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) . T)) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) . T)) ((((-380 |#2|)) . T) (((-380 (-520))) . T) (($) . T)) ((((-611 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1556,7 +1556,7 @@ (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012)))) ((($ $) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((($ $) . T)) ((((-520) (-108)) . T)) ((($) . T)) @@ -1585,7 +1585,7 @@ (((|#1| (-1128 |#1| |#2| |#3|)) . T)) (((|#1| (-706)) . T)) (((|#1|) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-791)) . T)) (|has| |#1| (-1012)) ((((-1066) |#1|) . T)) @@ -1624,7 +1624,7 @@ (|has| |#1| (-512)) (((|#1|) . T)) ((((-791)) . T)) -(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) (((|#1|) |has| |#1| (-157))) ((($) |has| |#1| (-512)) ((|#1|) |has| |#1| (-157)) (((-380 (-520))) |has| |#1| (-37 (-380 (-520))))) (((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) @@ -1642,7 +1642,7 @@ (|has| |#1| (-781)) (((|#1| (-520) (-997)) . T)) (-3700 (|has| |#1| (-828 (-1083))) (|has| |#1| (-969))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#1| (-380 (-520)) (-997)) . T)) (((|#1| (-706) (-997)) . T)) (|has| |#1| (-783)) @@ -1661,8 +1661,8 @@ (-3700 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-336)) (|has| |#2| (-341)) (|has| |#2| (-728)) (|has| |#2| (-781)) (|has| |#2| (-969)) (|has| |#2| (-1012))) (((|#2|) |has| |#2| (-157))) (((|#1|) |has| |#1| (-157))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) ((((-791)) . T)) (|has| |#3| (-781)) ((((-791)) . T)) @@ -1676,9 +1676,9 @@ (((|#2|) |has| |#2| (-336))) ((($) . T) ((|#1|) . T) (((-380 (-520))) |has| |#1| (-336))) (|has| |#1| (-783)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) |has| (-2 (|:| -2534 (-1083)) (|:| -3049 (-51))) (-283 (-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))))) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) |has| (-2 (|:| -2526 (-1083)) (|:| -3043 (-51))) (-283 (-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))))) (-3700 (|has| |#1| (-424)) (|has| |#1| (-837))) (((|#2|) . T) (((-520)) |has| |#2| (-582 (-520)))) ((((-791)) . T)) @@ -1724,7 +1724,7 @@ (|has| (-380 |#2|) (-209)) (|has| |#1| (-837)) (((|#2|) |has| |#2| (-969))) -(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) (|has| |#1| (-336)) (((|#1|) |has| |#1| (-157))) (((|#1| |#1|) . T)) @@ -1771,13 +1771,13 @@ ((((-108)) |has| |#1| (-1012)) (((-791)) -3700 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-157)) (|has| |#1| (-336)) (|has| |#1| (-445)) (|has| |#1| (-662)) (|has| |#1| (-828 (-1083))) (|has| |#1| (-969)) (|has| |#1| (-1024)) (|has| |#1| (-1012)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 (-51)))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 (-51)))) . T)) ((((-791)) . T)) ((((-520) |#1|) . T)) ((((-635)) . T) (((-380 (-520))) . T) (((-520)) . T)) (((|#1| |#1|) |has| |#1| (-157))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) ((((-352)) . T)) ((((-635)) . T)) ((((-380 (-520))) . #0=(|has| |#2| (-336))) (($) . #0#)) @@ -1795,7 +1795,7 @@ (|has| |#1| (-783)) ((((-1083)) |has| |#2| (-828 (-1083)))) ((((-791)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-380 (-520))) . T) (($) . T)) (|has| |#1| (-445)) (|has| |#1| (-341)) @@ -1823,11 +1823,11 @@ (|has| |#1| (-37 (-380 (-520)))) (|has| |#1| (-37 (-380 (-520)))) (|has| |#1| (-783)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-135)) (|has| |#1| (-133)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)))) ((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012)))) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)))) ((|#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012)))) (((|#2|) . T)) (((|#3|) . T)) ((((-112 |#1|)) . T)) @@ -1845,7 +1845,7 @@ ((((-496)) |has| |#1| (-561 (-496))) (((-820 (-520))) |has| |#1| (-561 (-820 (-520)))) (((-820 (-352))) |has| |#1| (-561 (-820 (-352)))) (((-352)) . #0=(|has| |#1| (-945))) (((-201)) . #0#)) (((|#1|) |has| |#1| (-336))) ((((-791)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((($ $) . T) (((-559 $) $) . T)) (-3700 (|has| |#1| (-336)) (|has| |#1| (-512))) ((($) . T) (((-1150 |#1| |#2| |#3| |#4|)) . T) (((-380 (-520))) . T)) @@ -1903,7 +1903,7 @@ ((((-791)) . T)) (((|#3|) . T)) (((|#1| |#1|) . T) (($ $) -3700 (|has| |#1| (-264)) (|has| |#1| (-336))) ((#0=(-380 (-520)) #0#) |has| |#1| (-336))) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) . T)) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) . T)) ((($) . T)) ((((-520) |#1|) . T)) ((((-1083)) |has| (-380 |#2|) (-828 (-1083)))) @@ -1942,7 +1942,7 @@ ((($) -3700 (|has| |#1| (-336)) (|has| |#1| (-322))) (((-380 (-520))) -3700 (|has| |#1| (-336)) (|has| |#1| (-322))) ((|#1|) . T)) ((((-520)) . T)) (|has| |#1| (-37 (-380 (-520)))) -((((-2 (|:| -2534 (-1066)) (|:| -3049 (-51)))) |has| (-2 (|:| -2534 (-1066)) (|:| -3049 (-51))) (-283 (-2 (|:| -2534 (-1066)) (|:| -3049 (-51)))))) +((((-2 (|:| -2526 (-1066)) (|:| -3043 (-51)))) |has| (-2 (|:| -2526 (-1066)) (|:| -3043 (-51))) (-283 (-2 (|:| -2526 (-1066)) (|:| -3043 (-51)))))) (((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) (|has| |#1| (-781)) (|has| |#1| (-37 (-380 (-520)))) @@ -1981,10 +1981,10 @@ (((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) ((((-496)) |has| |#4| (-561 (-496)))) ((((-791)) . T) (((-586 |#4|)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-781)) -(((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012))) (((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) |has| (-2 (|:| -2534 (-1066)) (|:| -3049 |#1|)) (-283 (-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))))) +(((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012))) (((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) |has| (-2 (|:| -2526 (-1066)) (|:| -3043 |#1|)) (-283 (-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))))) (|has| |#1| (-1012)) (|has| |#1| (-336)) (|has| |#1| (-783)) @@ -2024,7 +2024,7 @@ ((((-791)) . T)) ((((-791)) . T)) ((((-496)) |has| |#1| (-561 (-496)))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-1083) |#1|) |has| |#1| (-481 (-1083) |#1|)) ((|#1| |#1|) |has| |#1| (-283 |#1|))) (((|#1|) -3700 (|has| |#1| (-157)) (|has| |#1| (-336)))) ((((-289 |#1|)) . T)) @@ -2051,7 +2051,7 @@ (|has| |#1| (-512)) (((|#2|) . T)) ((((-520)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (-3700 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-512)) (|has| |#1| (-969))) @@ -2164,14 +2164,14 @@ (|has| |#2| (-837)) (|has| |#1| (-837)) (((|#2|) |has| |#2| (-157))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-1156 |#1| |#2| |#3|)) |has| |#1| (-336))) ((((-791)) . T)) ((((-791)) . T)) ((((-496)) . T) (((-520)) . T) (((-820 (-520))) . T) (((-352)) . T) (((-201)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 (-51)))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 (-51)))) . T)) (((|#1|) . T)) ((((-791)) . T)) (((|#1| |#2|) . T)) @@ -2192,7 +2192,7 @@ ((((-380 (-520))) . T) (($) . T)) ((((-791)) . T)) ((((-791)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-791)) . T)) ((((-791)) . T)) @@ -2203,7 +2203,7 @@ (((|#1|) . T)) ((((-586 (-132))) . T) (((-1066)) . T)) ((((-791)) . T)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) ((((-1083) |#1|) |has| |#1| (-481 (-1083) |#1|)) ((|#1| |#1|) |has| |#1| (-283 |#1|))) (|has| |#1| (-783)) ((((-791)) . T)) @@ -2257,8 +2257,8 @@ (-3700 (|has| |#1| (-133)) (|has| |#1| (-341))) (-3700 (|has| |#1| (-133)) (|has| |#1| (-341))) (-3700 (|has| |#1| (-133)) (|has| |#1| (-341))) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) . T)) -(((#0=(-51)) . T) (((-2 (|:| -2534 (-1083)) (|:| -3049 #0#))) . T)) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -2526 (-1083)) (|:| -3043 #0#))) . T)) (|has| |#1| (-322)) ((((-520)) . T)) ((((-791)) . T)) @@ -2328,7 +2328,7 @@ (|has| |#2| (-945)) ((($) . T)) (|has| |#1| (-837)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2345,12 +2345,12 @@ ((((-380 |#2|) |#3|) . T)) ((($) . T) (((-380 (-520))) . T)) ((((-706) |#1|) . T)) -(((|#2| (-216 (-3479 |#1|) (-706))) . T)) +(((|#2| (-216 (-3474 |#1|) (-706))) . T)) (((|#1| (-492 |#3|)) . T)) ((((-380 (-520))) . T)) (-3700 (|has| |#1| (-424)) (|has| |#1| (-512)) (|has| |#1| (-837))) ((((-791)) . T)) -(((#0=(-2 (|:| -2534 (-1083)) (|:| -3049 (-51))) #0#) |has| (-2 (|:| -2534 (-1083)) (|:| -3049 (-51))) (-283 (-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))))) +(((#0=(-2 (|:| -2526 (-1083)) (|:| -3043 (-51))) #0#) |has| (-2 (|:| -2526 (-1083)) (|:| -3043 (-51))) (-283 (-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))))) (|has| |#1| (-837)) (|has| |#2| (-336)) (-3700 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-336)) (|has| |#2| (-728)) (|has| |#2| (-781)) (|has| |#2| (-969))) @@ -2384,7 +2384,7 @@ (((|#1|) . T)) (((|#2|) |has| |#1| (-336))) (((|#2|) |has| |#1| (-336))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-157))) (((|#1|) . T)) @@ -2420,9 +2420,9 @@ (((|#2|) . T)) (((|#2|) . T)) (-3700 (|has| |#2| (-157)) (|has| |#2| (-781)) (|has| |#2| (-969))) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (|has| |#1| (-37 (-380 (-520)))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-380 (-520)))) @@ -2535,7 +2535,7 @@ (|has| |#1| (-209)) (((|#1| (-492 (-1002 (-1083)))) . T)) (|has| |#2| (-336)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 (-51)))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 (-51)))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-283 |#1|)) (|has| |#1| (-1012)))) ((((-791)) . T)) @@ -2584,7 +2584,7 @@ (|has| |#1| (-837)) ((($) -3700 (|has| |#1| (-157)) (|has| |#1| (-424)) (|has| |#1| (-512)) (|has| |#1| (-837))) ((|#1|) . T) (((-380 (-520))) |has| |#1| (-37 (-380 (-520))))) (((|#1|) . T)) -((((-2 (|:| -2534 (-1066)) (|:| -3049 |#1|))) . T)) +((((-2 (|:| -2526 (-1066)) (|:| -3043 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) . T)) @@ -2697,7 +2697,7 @@ (((|#1|) . T)) ((((-791)) . T)) (|has| |#2| (-837)) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) . T)) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) . T)) ((((-496)) |has| |#2| (-561 (-496))) (((-820 (-352))) |has| |#2| (-561 (-820 (-352)))) (((-820 (-520))) |has| |#2| (-561 (-820 (-520))))) ((((-791)) . T)) ((((-791)) . T)) @@ -2730,7 +2730,7 @@ ((((-380 |#2|) |#3|) . T)) (((|#1|) . T)) (|has| |#1| (-1012)) -(((|#2| (-453 (-3479 |#1|) (-706))) . T)) +(((|#2| (-453 (-3474 |#1|) (-706))) . T)) ((((-520) |#1|) . T)) (((|#2| |#2|) . T)) (((|#1| (-492 (-1083))) . T)) @@ -2785,7 +2785,7 @@ (|has| |#1| (-209)) (((|#1| (-492 |#3|)) . T)) (|has| |#1| (-341)) -(((|#2| (-216 (-3479 |#1|) (-706))) . T)) +(((|#2| (-216 (-3474 |#1|) (-706))) . T)) (|has| |#1| (-341)) (|has| |#1| (-341)) (((|#1|) . T) (($) . T)) @@ -2847,7 +2847,7 @@ ((((-791)) -3700 (|has| |#1| (-560 (-791))) (|has| |#1| (-783)) (|has| |#1| (-1012)))) ((((-496)) |has| |#1| (-561 (-496)))) ((((-791)) . T)) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) |has| (-2 (|:| -2534 (-1083)) (|:| -3049 (-51))) (-283 (-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))))) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) |has| (-2 (|:| -2526 (-1083)) (|:| -3043 (-51))) (-283 (-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))))) (-3700 (|has| |#2| (-424)) (|has| |#2| (-512)) (|has| |#2| (-837))) ((((-520) |#1|) . T)) ((((-520) |#1|) . T)) @@ -3018,7 +3018,7 @@ (-3700 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-728)) (|has| |#2| (-728)))) ((((-520)) . T)) ((((-520)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) (-3700 (|has| |#2| (-157)) (|has| |#2| (-781)) (|has| |#2| (-969))) @@ -3108,11 +3108,11 @@ ((((-1081 |#1| |#2| |#3|)) |has| |#1| (-336))) ((((-1081 |#1| |#2| |#3|)) |has| |#1| (-336))) ((((-1048 |#1| |#2|)) . T)) -(((|#2|) . T) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) . T)) +(((|#2|) . T) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) . T)) ((($) . T)) (|has| |#1| (-945)) -(((|#2|) . T) (((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) ((((-791)) . T)) ((((-496)) |has| |#2| (-561 (-496))) (((-820 (-520))) |has| |#2| (-561 (-820 (-520)))) (((-820 (-352))) |has| |#2| (-561 (-820 (-352)))) (((-352)) . #0=(|has| |#2| (-945))) (((-201)) . #0#)) ((((-1083) (-51)) . T)) @@ -3157,7 +3157,7 @@ ((((-791)) . T)) ((((-791)) . T)) (((|#1| (-492 |#2|)) . T)) -((((-2 (|:| -2534 (-1083)) (|:| -3049 (-51)))) . T)) +((((-2 (|:| -2526 (-1083)) (|:| -3043 (-51)))) . T)) (((|#1| (-520)) . T)) (((|#1| (-380 (-520))) . T)) (((|#1| (-706)) . T)) @@ -3174,7 +3174,7 @@ (((|#1| |#2|) . T)) ((((-1066) |#1|) . T)) ((((-380 |#2|)) . T)) -((((-2 (|:| -2534 |#1|) (|:| -3049 |#2|))) . T)) +((((-2 (|:| -2526 |#1|) (|:| -3043 |#2|))) . T)) (|has| |#1| (-512)) (|has| |#1| (-512)) ((($) . T) ((|#2|) . T)) @@ -3198,7 +3198,7 @@ (((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1048 |#1| |#2|) #0#) |has| (-1048 |#1| |#2|) (-283 (-1048 |#1| |#2|)))) -(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) #0#) |has| (-2 (|:| -2534 |#1|) (|:| -3049 |#2|)) (-283 (-2 (|:| -2534 |#1|) (|:| -3049 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-283 |#2|)) (|has| |#2| (-1012))) ((#0=(-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) #0#) |has| (-2 (|:| -2526 |#1|) (|:| -3043 |#2|)) (-283 (-2 (|:| -2526 |#1|) (|:| -3043 |#2|))))) (((#0=(-112 |#1|)) |has| #0# (-283 #0#))) (-3700 (|has| |#1| (-783)) (|has| |#1| (-1012))) ((($ $) . T)) |