aboutsummaryrefslogtreecommitdiff
path: root/src/share/algebra/category.daase
diff options
context:
space:
mode:
Diffstat (limited to 'src/share/algebra/category.daase')
-rw-r--r--src/share/algebra/category.daase222
1 files changed, 111 insertions, 111 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase
index dba73988..794b9022 100644
--- a/src/share/algebra/category.daase
+++ b/src/share/algebra/category.daase
@@ -1,6 +1,6 @@
-(188029 . 3453749799)
-(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(188029 . 3453990502)
+(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
((((-566)) . T) (($) -2805 (|has| |#1| (-308)) (|has| |#1| (-365)) (|has| |#1| (-351)) (|has| |#1| (-558))) (((-409 (-566))) -2805 (|has| |#1| (-365)) (|has| |#1| (-351)) (|has| |#1| (-1038 (-409 (-566))))) ((|#1|) . T))
(((|#2| |#2|) . T))
((((-566)) . T))
@@ -51,12 +51,12 @@
(((|#1|) . T) (((-566)) |has| |#1| (-1038 (-566))) (((-409 (-566))) |has| |#1| (-1038 (-409 (-566)))))
(-2805 (|has| |#2| (-172)) (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909)))
(-2805 (|has| |#1| (-172)) (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909)))
-(((|#2| (-484 (-2997 |#1|) (-771))) . T))
+(((|#2| (-484 (-3020 |#1|) (-771))) . T))
(((|#1| (-533 (-1175))) . T))
(((#0=(-870 |#1|) #0#) . T) ((#1=(-409 (-566)) #1#) . T) (($ $) . T))
((((-1157)) . T) (((-958 (-129))) . T) (((-862)) . T))
((((-862)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(|has| |#4| (-370))
(|has| |#3| (-370))
(((|#1|) . T))
@@ -73,7 +73,7 @@
((((-566)) . T) (((-409 (-566))) -2805 (|has| |#2| (-38 (-409 (-566)))) (|has| |#2| (-1038 (-409 (-566))))) ((|#2|) . T) (($) -2805 (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909))) (((-864 |#1|)) . T))
(-2805 (|has| |#1| (-365)) (|has| |#1| (-558)))
(-2805 (|has| |#1| (-365)) (|has| |#1| (-558)))
-((((-2 (|:| -2168 |#1|) (|:| -3250 |#2|))) . T))
+((((-2 (|:| -2208 |#1|) (|:| -2456 |#2|))) . T))
((($) . T))
((((-566)) . T) (((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-1038 (-409 (-566))))) ((|#1|) . T) (($) -2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) (((-1175)) . T))
((((-862)) -2805 (|has| |#1| (-613 (-862))) (|has| |#1| (-850)) (|has| |#1| (-1099))))
@@ -129,7 +129,7 @@
(((|#1|) . T) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))) (($) . T))
(-2805 (|has| |#1| (-850)) (|has| |#1| (-1099)))
(((|#1|) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-566)) . T))
((((-862)) . T))
(((|#1| |#2|) . T))
@@ -268,8 +268,8 @@
(((|#1|) . T))
((((-409 (-566))) |has| |#1| (-1038 (-409 (-566)))) (((-566)) |has| |#1| (-1038 (-566))) ((|#1|) . T))
(((|#1|) . T) (((-566)) |has| |#1| (-639 (-566))))
-(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
-(((|#1|) . T) (((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
+(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
+(((|#1|) . T) (((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
(|has| |#1| (-558))
((((-566)) -2805 (|has| |#4| (-172)) (|has| |#4| (-848)) (-12 (|has| |#4| (-1038 (-566))) (|has| |#4| (-1099))) (|has| |#4| (-1049))) ((|#4|) -2805 (|has| |#4| (-172)) (|has| |#4| (-1099))) (((-409 (-566))) -12 (|has| |#4| (-1038 (-409 (-566)))) (|has| |#4| (-1099))))
((((-566)) -2805 (|has| |#3| (-172)) (|has| |#3| (-848)) (-12 (|has| |#3| (-1038 (-566))) (|has| |#3| (-1099))) (|has| |#3| (-1049))) ((|#3|) -2805 (|has| |#3| (-172)) (|has| |#3| (-1099))) (((-409 (-566))) -12 (|has| |#3| (-1038 (-409 (-566)))) (|has| |#3| (-1099))))
@@ -298,11 +298,11 @@
((((-538)) |has| |#2| (-614 (-538))) (((-892 (-381))) |has| |#2| (-614 (-892 (-381)))) (((-892 (-566))) |has| |#2| (-614 (-892 (-566)))))
((((-862)) . T))
(((|#1| |#2| |#3| |#4|) . T))
-((((-2 (|:| -2168 |#1|) (|:| -3250 |#2|))) . T) (((-862)) . T))
+((((-2 (|:| -2208 |#1|) (|:| -2456 |#2|))) . T) (((-862)) . T))
((((-538)) |has| |#1| (-614 (-538))) (((-892 (-381))) |has| |#1| (-614 (-892 (-381)))) (((-892 (-566))) |has| |#1| (-614 (-892 (-566)))))
(((|#4|) -2805 (|has| |#4| (-172)) (|has| |#4| (-365)) (|has| |#4| (-1049))) (($) |has| |#4| (-172)))
(((|#3|) -2805 (|has| |#3| (-172)) (|has| |#3| (-365)) (|has| |#3| (-1049))) (($) |has| |#3| (-172)))
-((((-2 (|:| -2168 |#1|) (|:| -3250 |#2|))) . T))
+((((-2 (|:| -2208 |#1|) (|:| -2456 |#2|))) . T))
((((-862)) . T))
((((-862)) . T))
((((-538)) . T) (((-566)) . T) (((-892 (-566))) . T) (((-381)) . T) (((-225)) . T))
@@ -310,7 +310,7 @@
(((|#1|) . T) (((-566)) |has| |#1| (-1038 (-566))) (((-409 (-566))) |has| |#1| (-1038 (-409 (-566)))))
((($) . T) (((-409 (-566))) |has| |#2| (-38 (-409 (-566)))) ((|#2|) . T))
((((-409 $) (-409 $)) |has| |#2| (-558)) (($ $) . T) ((|#2| |#2|) . T))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) . T))
(((|#1|) . T))
(|has| |#2| (-909))
((((-1157) (-52)) . T))
@@ -349,7 +349,7 @@
(((|#1|) . T))
(((|#2| |#2|) . T))
(|has| |#1| (-1150))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
(|has| (-1250 |#1| |#2| |#3| |#4|) (-145))
(|has| (-1250 |#1| |#2| |#3| |#4|) (-147))
(|has| |#1| (-145))
@@ -367,10 +367,10 @@
((($) . T) ((|#1|) . T))
(((|#2|) |has| |#2| (-1049)))
((((-862)) . T))
-(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
(((|#1|) . T))
-((((-1264 (-341 (-2523) (-2523 (QUOTE X)) (-699)))) . T))
-(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) ((#0=(-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) #0#) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)))))
+((((-1264 (-341 (-3791) (-3791 (QUOTE X)) (-699)))) . T))
+(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) ((#0=(-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) #0#) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)))))
((((-862)) . T))
((((-566) |#1|) . T))
((((-538)) -12 (|has| |#1| (-614 (-538))) (|has| |#2| (-614 (-538)))) (((-892 (-381))) -12 (|has| |#1| (-614 (-892 (-381)))) (|has| |#2| (-614 (-892 (-381))))) (((-892 (-566))) -12 (|has| |#1| (-614 (-892 (-566)))) (|has| |#2| (-614 (-892 (-566))))))
@@ -488,12 +488,12 @@
((((-144)) . T))
(((|#3|) |has| |#3| (-1099)) (((-566)) -12 (|has| |#3| (-1038 (-566))) (|has| |#3| (-1099))) (((-409 (-566))) -12 (|has| |#3| (-1038 (-409 (-566)))) (|has| |#3| (-1099))))
((((-862)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#1|) . T))
((((-862)) -2805 (|has| |#1| (-613 (-862))) (|has| |#1| (-850)) (|has| |#1| (-1099))))
((((-538)) |has| |#1| (-614 (-538))))
(((|#1|) |has| |#1| (-172)))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T))
(|has| |#1| (-365))
((((-1180)) . T))
(((|#1|) . T))
@@ -504,13 +504,13 @@
(|has| |#1| (-848))
(-2805 (|has| |#1| (-850)) (|has| |#1| (-1099)))
((((-862)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-538)) |has| |#1| (-614 (-538))))
(((|#1| |#2|) . T))
((((-1175)) -12 (|has| |#1| (-365)) (|has| |#1| (-900 (-1175)))))
((((-1157) |#1|) . T))
(((|#1| |#2| |#3| (-533 |#3|)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(|has| |#1| (-370))
(|has| |#1| (-370))
(|has| |#1| (-370))
@@ -726,7 +726,7 @@
((((-1139 |#1| |#2|)) |has| (-1139 |#1| |#2|) (-310 (-1139 |#1| |#2|))))
(((|#4| |#4|) -12 (|has| |#4| (-310 |#4|)) (|has| |#4| (-1099))))
(((|#3| |#3|) -12 (|has| |#3| (-310 |#3|)) (|has| |#3| (-1099))))
-(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
(((|#2|) . T) (((-566)) |has| |#2| (-1038 (-566))) (((-409 (-566))) |has| |#2| (-1038 (-409 (-566)))))
(((|#1|) . T))
(((|#1| |#2|) . T))
@@ -735,7 +735,7 @@
(((|#2|) . T))
(((|#3|) . T))
(-2805 (|has| |#1| (-850)) (|has| |#1| (-1099)))
-(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
(((|#2|) . T))
((((-862)) -2805 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-613 (-862))) (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-370)) (|has| |#2| (-726)) (|has| |#2| (-793)) (|has| |#2| (-848)) (|has| |#2| (-1049)) (|has| |#2| (-1099))) (((-1264 |#2|)) . T))
((((-409 (-566))) |has| |#1| (-1038 (-409 (-566)))) ((|#1|) . T) (((-566)) . T) (($) . T))
@@ -834,9 +834,9 @@
(-2805 (|has| |#1| (-454)) (|has| |#1| (-909)))
((((-566) |#2|) . T))
((((-862)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))))
((($) -2805 (|has| |#3| (-172)) (|has| |#3| (-848)) (|has| |#3| (-1049))) ((|#3|) -2805 (|has| |#3| (-172)) (|has| |#3| (-365)) (|has| |#3| (-1049))))
((((-566) |#1|) . T))
@@ -851,11 +851,11 @@
(|has| |#1| (-558))
(|has| |#1| (-38 (-409 (-566))))
(|has| |#1| (-38 (-409 (-566))))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-862)) . T))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
(|has| |#1| (-38 (-409 (-566))))
-((((-390) (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
+((((-390) (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
(|has| |#1| (-38 (-409 (-566))))
(|has| |#2| (-1150))
(-2805 (|has| |#1| (-365)) (|has| |#1| (-558)))
@@ -1070,7 +1070,7 @@
(|has| |#1| (-147))
(|has| |#1| (-145))
(|has| |#4| (-848))
-(((|#2| (-240 (-2997 |#1|) (-771)) (-864 |#1|)) . T))
+(((|#2| (-240 (-3020 |#1|) (-771)) (-864 |#1|)) . T))
(|has| |#3| (-848))
(((|#1| (-533 |#3|) |#3|) . T))
(|has| |#1| (-147))
@@ -1091,7 +1091,7 @@
(|has| |#2| (-172))
(((|#1| |#2|) . T))
(-12 (|has| |#2| (-233)) (|has| |#2| (-1049)))
-(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(-2805 (|has| |#3| (-793)) (|has| |#3| (-848)))
(-2805 (|has| |#3| (-793)) (|has| |#3| (-848)))
((((-862)) . T))
@@ -1122,10 +1122,10 @@
(((|#1| (-409 (-566))) . T))
(((|#3|) . T) (((-612 $)) . T))
(((|#1| |#2|) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#1|) . T))
(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-566)) -2805 (|has| |#2| (-172)) (|has| |#2| (-848)) (-12 (|has| |#2| (-1038 (-566))) (|has| |#2| (-1099))) (|has| |#2| (-1049))) ((|#2|) -2805 (|has| |#2| (-172)) (|has| |#2| (-1099))) (((-409 (-566))) -12 (|has| |#2| (-1038 (-409 (-566)))) (|has| |#2| (-1099))))
(((|#1|) . T) (((-409 (-566))) . T) (($) . T))
((($ $) . T) ((|#2| $) . T))
@@ -1134,8 +1134,8 @@
((((-862)) . T))
((((-862)) . T))
(((|#1| |#1|) . T))
-(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
-(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) (((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)))))
+(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
+(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) (((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)))))
((((-862)) . T))
(((|#1|) . T))
(((|#3| |#3|) . T))
@@ -1151,7 +1151,7 @@
(|has| |#1| (-1099))
(((|#2| |#2|) -2805 (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-1049))) (($ $) |has| |#2| (-172)))
(((|#2|) -2805 (|has| |#2| (-172)) (|has| |#2| (-365))))
-((((-566) (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T) ((|#1| |#2|) . T))
+((((-566) (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T) ((|#1| |#2|) . T))
(((|#2|) -2805 (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-1049))) (($) |has| |#2| (-172)))
((((-566)) . T))
((((-1180)) . T))
@@ -1195,7 +1195,7 @@
(-2805 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-370)) (|has| |#2| (-726)) (|has| |#2| (-793)) (|has| |#2| (-848)) (|has| |#2| (-1049)) (|has| |#2| (-1099)))
(-12 (|has| |#3| (-233)) (|has| |#3| (-1049)))
(|has| |#2| (-1150))
-(((#0=(-52)) . T) (((-2 (|:| -2010 (-1175)) (|:| -2818 #0#))) . T))
+(((#0=(-52)) . T) (((-2 (|:| -2050 (-1175)) (|:| -2849 #0#))) . T))
(((|#1| |#2|) . T))
(-2805 (|has| |#3| (-172)) (|has| |#3| (-848)) (|has| |#3| (-1049)))
(((|#1| (-566) (-1081)) . T))
@@ -1224,7 +1224,7 @@
(((|#4|) . T) (((-862)) . T))
(((|#3|) . T) ((|#2|) . T) (($) -2805 (|has| |#4| (-172)) (|has| |#4| (-848)) (|has| |#4| (-1049))) (((-566)) . T) ((|#4|) -2805 (|has| |#4| (-172)) (|has| |#4| (-365)) (|has| |#4| (-1049))))
(((|#2|) . T) (($) -2805 (|has| |#3| (-172)) (|has| |#3| (-848)) (|has| |#3| (-1049))) (((-566)) . T) ((|#3|) -2805 (|has| |#3| (-172)) (|has| |#3| (-365)) (|has| |#3| (-1049))))
-(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
(|has| |#1| (-558))
(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))))
((((-862)) . T))
@@ -1284,7 +1284,7 @@
(-12 (|has| |#1| (-793)) (|has| |#2| (-793)))
(-2805 (|has| |#2| (-172)) (|has| |#2| (-848)) (|has| |#2| (-1049)))
((($) . T) (((-566)) . T) ((|#2|) . T))
-(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#2|) . T) (($) . T))
(|has| |#1| (-1199))
(((#0=(-566) #0#) . T) ((#1=(-409 (-566)) #1#) . T) (($ $) . T))
@@ -1315,7 +1315,7 @@
((($) . T) (((-409 (-566))) -2805 (|has| |#1| (-365)) (|has| |#1| (-351))) ((|#1|) . T))
(-2805 (|has| |#1| (-172)) (|has| |#1| (-558)))
((($) . T))
-(((#0=(-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) #0#) |has| (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))))))
+(((#0=(-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) #0#) |has| (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))))))
((($) . T))
((($) . T))
(((|#2|) |has| |#2| (-1099)))
@@ -1331,10 +1331,10 @@
((((-566)) |has| #0=(-409 |#2|) (-639 (-566))) ((#0#) . T))
((($) . T) (((-566)) . T))
((((-566) (-144)) . T))
-((((-566) (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T) ((|#1| |#2|) . T))
+((((-566) (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T) ((|#1| |#2|) . T))
((((-409 (-566))) . T) (($) . T))
(((|#1|) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-862)) . T))
((((-910 |#1|)) . T))
(|has| |#1| (-365))
@@ -1363,7 +1363,7 @@
((((-862)) . T))
((($) . T))
(((|#2|) . T) (($) . T))
-((((-566) (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T) ((|#1| |#2|) . T))
+((((-566) (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T) ((|#1| |#2|) . T))
(((|#1|) . T))
(((|#1|) |has| |#1| (-172)))
((($) |has| |#1| (-558)) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))))
@@ -1378,7 +1378,7 @@
((((-538)) |has| |#1| (-614 (-538))) (((-892 (-381))) |has| |#1| (-614 (-892 (-381)))) (((-892 (-566))) |has| |#1| (-614 (-892 (-566)))))
((((-862)) . T))
((((-870 |#1|)) . T) (($) . T) (((-409 (-566))) . T))
-(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-508)) . T))
(|has| |#2| (-848))
((((-508)) . T))
@@ -1413,7 +1413,7 @@
(((|#1|) . T))
((((-1175)) |has| (-409 |#2|) (-900 (-1175))))
(((|#2|) . T))
-(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
((((-409 (-566))) |has| |#2| (-38 (-409 (-566)))) ((|#2|) |has| |#2| (-172)) (($) -2805 (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909))))
((((-409 (-566))) |has| |#2| (-38 (-409 (-566)))) ((|#2|) . T) (($) -2805 (|has| |#2| (-172)) (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909))))
((((-409 (-566))) |has| |#1| (-38 (-409 (-566)))) ((|#1|) |has| |#1| (-172)) (($) -2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))))
@@ -1430,7 +1430,7 @@
(((|#2|) . T) (((-566)) . T))
((((-862)) . T))
((((-862)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T) ((|#2|) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T) ((|#2|) . T))
((((-862)) . T))
((((-862)) . T))
((((-1157) (-1175) (-566) (-225) (-862)) . T))
@@ -1521,7 +1521,7 @@
((((-999 |#1|)) . T) ((|#1|) . T))
((((-862)) . T))
((((-862)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-409 (-566))) . T) (((-409 |#1|)) . T) ((|#1|) . T) (($) . T))
(((|#1| (-1171 |#1|)) . T))
((((-566)) . T) (($) . T) (((-409 (-566))) . T))
@@ -1530,7 +1530,7 @@
(((|#1|) . T) (((-566)) . T) (($) . T))
(((|#2|) . T))
((((-566)) . T) (($) . T) (((-409 (-566))) . T))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
((((-862)) -2805 (|has| |#1| (-613 (-862))) (|has| |#1| (-1099))))
((((-566) |#2|) . T))
(((|#1|) . T) (((-409 (-566))) . T) (((-566)) . T) (($) . T))
@@ -1544,7 +1544,7 @@
(|has| |#1| (-38 (-409 (-566))))
(|has| |#1| (-38 (-409 (-566))))
((((-1256 |#1| |#2| |#3|)) |has| |#1| (-365)))
-(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
(((|#2| |#2|) . T))
(|has| |#1| (-1099))
(|has| |#1| (-38 (-409 (-566))))
@@ -1589,7 +1589,7 @@
(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))))
(((|#1| |#2|) . T))
((((-566) (-144)) . T))
-(((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))))
+(((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))))
((($) -2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))))
(|has| |#1| (-850))
(((|#2| (-771) (-1081)) . T))
@@ -1642,7 +1642,7 @@
((((-390) (-1157)) . T))
((($) |has| |#1| (-558)) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))))
((((-862)) -2805 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-613 (-862))) (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-370)) (|has| |#2| (-726)) (|has| |#2| (-793)) (|has| |#2| (-848)) (|has| |#2| (-1049)) (|has| |#2| (-1099))) (((-1264 |#2|)) . T))
-(((#0=(-52)) . T) (((-2 (|:| -2010 (-1157)) (|:| -2818 #0#))) . T))
+(((#0=(-52)) . T) (((-2 (|:| -2050 (-1157)) (|:| -2849 #0#))) . T))
(((|#1|) . T))
((((-862)) . T))
(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))))
@@ -1672,7 +1672,7 @@
((((-862)) . T))
((((-862)) . T))
(|has| |#1| (-1099))
-(((|#2| (-484 (-2997 |#1|) (-771)) (-864 |#1|)) . T))
+(((|#2| (-484 (-3020 |#1|) (-771)) (-864 |#1|)) . T))
((((-409 (-566))) . #0=(|has| |#2| (-365))) (($) . #0#))
(((|#1| (-533 (-1175)) (-1175)) . T))
(((|#1|) . T))
@@ -1693,12 +1693,12 @@
(((|#2|) |has| |#2| (-172)))
(((|#1|) . T))
(((|#2|) . T))
-(((|#1|) . T) (((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+(((|#1|) . T) (((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#2|) . T))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T))
((((-1173 |#1| |#2| |#3|)) |has| |#1| (-365)))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-1175) (-52)) . T))
((($ $) . T))
(((|#1| (-566)) . T))
@@ -1748,11 +1748,11 @@
(-2805 (|has| |#1| (-365)) (|has| |#1| (-351)))
(|has| |#1| (-38 (-409 (-566))))
(|has| |#1| (-38 (-409 (-566))))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-1175)) |has| |#1| (-900 (-1175))) (((-1081)) . T))
(((|#1|) . T))
(|has| |#1| (-848))
-(((#0=(-2 (|:| -2010 (-1157)) (|:| -2818 (-52))) #0#) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 (-52))))))
+(((#0=(-2 (|:| -2050 (-1157)) (|:| -2849 (-52))) #0#) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 (-52))))))
(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))))
(|has| |#1| (-1099))
((((-862)) . T) (((-1180)) . T))
@@ -1812,7 +1812,7 @@
(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))))
(((|#1|) . T))
(((|#1| |#2|) . T))
-(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) ((#0=(-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) #0#) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)))))
+(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) ((#0=(-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) #0#) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)))))
(-2805 (|has| |#2| (-454)) (|has| |#2| (-909)))
(-2805 (|has| |#1| (-454)) (|has| |#1| (-909)))
(((|#1|) . T) (($) . T))
@@ -1837,7 +1837,7 @@
((((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-365))) (($) -2805 (|has| |#1| (-365)) (|has| |#1| (-558))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-365)) ((|#1|) |has| |#1| (-172)))
(((|#1|) |has| |#1| (-172)) (((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-365))) (($) -2805 (|has| |#1| (-365)) (|has| |#1| (-558))))
((($) |has| |#1| (-558)) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T))
((((-409 |#2|)) . T) (((-409 (-566))) . T) (($) . T))
((((-672 |#1|)) . T))
(((|#1| |#2| |#3| |#4|) . T))
@@ -1915,7 +1915,7 @@
((((-862)) . T))
((((-862)) . T))
((($ $) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((($ $) . T))
((((-566) (-112)) . T))
((($) . T))
@@ -1944,7 +1944,7 @@
(((|#1| (-1228 |#1| |#2| |#3|)) . T))
(((|#1| (-771)) . T))
(((|#1|) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-862)) . T))
(|has| |#1| (-1099))
((((-1157) |#1|) . T))
@@ -1991,7 +1991,7 @@
((($) -2805 (|has| |#1| (-172)) (|has| |#1| (-365)) (|has| |#1| (-558))) (((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-365))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-365)) ((|#1|) . T))
(((|#1|) . T) (($) -2805 (|has| |#1| (-172)) (|has| |#1| (-365)) (|has| |#1| (-558))) (((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-365))))
((($) -2805 (|has| |#1| (-172)) (|has| |#1| (-558))) ((|#1|) . T) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))))
-(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
(((|#1|) |has| |#1| (-172)))
((((-862)) . T))
((($) |has| |#1| (-558)) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))))
@@ -2015,7 +2015,7 @@
(|has| |#1| (-848))
(((|#1| (-566) (-1081)) . T))
(-2805 (|has| |#1| (-900 (-1175))) (|has| |#1| (-1049)))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#1| (-409 (-566)) (-1081)) . T))
(((|#1| (-771) (-1081)) . T))
(|has| |#1| (-850))
@@ -2034,11 +2034,11 @@
(|has| |#1| (-1099))
((((-566)) -12 (|has| |#1| (-365)) (|has| |#2| (-639 (-566)))) ((|#2|) |has| |#1| (-365)))
(-2805 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-370)) (|has| |#2| (-726)) (|has| |#2| (-793)) (|has| |#2| (-848)) (|has| |#2| (-1049)) (|has| |#2| (-1099)))
-((((-689 (-341 (-2523) (-2523 (QUOTE X) (QUOTE HESS)) (-699)))) . T))
+((((-689 (-341 (-3791) (-3791 (QUOTE X) (QUOTE HESS)) (-699)))) . T))
(((|#2|) |has| |#2| (-172)))
(((|#1|) |has| |#1| (-172)))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
((((-862)) . T))
(|has| |#3| (-848))
((((-862)) . T))
@@ -2054,11 +2054,11 @@
((($) . T) ((|#1|) . T) (((-409 (-566))) |has| |#1| (-365)))
(|has| |#1| (-850))
(((|#1|) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#1|) . T) (((-566)) . T))
(((|#2|) . T))
((((-566)) . T) ((|#3|) . T))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) |has| (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))))))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) |has| (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))))))
(-2805 (|has| |#1| (-454)) (|has| |#1| (-909)))
(((|#2|) . T) (((-566)) |has| |#2| (-639 (-566))))
((((-862)) . T))
@@ -2117,7 +2117,7 @@
((((-644 |#1|)) . T))
(|has| |#1| (-909))
(((|#2|) |has| |#2| (-1049)))
-(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
(|has| |#1| (-365))
(((|#1|) |has| |#1| (-172)))
(((|#1| |#1|) . T))
@@ -2169,7 +2169,7 @@
(((|#1| |#2|) . T))
((($) . T) (((-566)) . T) (((-409 (-566))) . T))
((((-566)) . T) (($) . T) (((-409 (-566))) . T))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) . T))
(((|#1|) . T) (((-409 (-566))) . T) (((-566)) . T) (($) . T))
(((|#1|) . T) (((-409 (-566))) . T) (((-566)) . T) (($) . T))
(((|#1|) . T) (((-409 (-566))) . T) (((-566)) . T) (($) . T))
@@ -2183,7 +2183,7 @@
(((|#2|) . T))
((($) . T) (((-566)) . T) (((-409 (-566))) -2805 (|has| |#1| (-365)) (|has| |#1| (-351))) ((|#1|) . T))
((((-566) |#1|) . T))
-(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
((((-381)) . T))
((((-699)) . T))
((((-409 (-566))) . #0=(|has| |#2| (-365))) (($) . #0#))
@@ -2200,7 +2200,7 @@
(|has| |#1| (-365))
((((-1175)) |has| |#2| (-900 (-1175))))
((((-862)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-409 (-566))) . T) (($) . T))
(|has| |#1| (-475))
(|has| |#1| (-370))
@@ -2228,12 +2228,12 @@
(|has| |#1| (-38 (-409 (-566))))
(|has| |#1| (-38 (-409 (-566))))
(|has| |#1| (-850))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
(((|#1| |#2|) . T))
((($) . T) (((-566)) . T))
(|has| |#1| (-147))
(|has| |#1| (-145))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))) ((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))) ((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))))
(((|#2|) . T))
(((|#3|) . T))
((((-116 |#1|)) . T))
@@ -2253,7 +2253,7 @@
((((-538)) |has| |#1| (-614 (-538))) (((-892 (-566))) |has| |#1| (-614 (-892 (-566)))) (((-892 (-381))) |has| |#1| (-614 (-892 (-381)))) (((-381)) . #0=(|has| |#1| (-1022))) (((-225)) . #0#))
(((|#1|) |has| |#1| (-365)))
((((-862)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((($ $) . T) (((-612 $) $) . T))
(-2805 (|has| |#1| (-365)) (|has| |#1| (-558)))
((($) . T) (((-1250 |#1| |#2| |#3| |#4|)) . T) (((-409 (-566))) . T))
@@ -2326,7 +2326,7 @@
((((-952 |#1|)) . T) (((-862)) . T))
(((|#3|) . T))
(((|#1| |#1|) . T) (($ $) -2805 (|has| |#1| (-291)) (|has| |#1| (-365))) ((#0=(-409 (-566)) #0#) |has| |#1| (-365)))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T))
((((-952 |#1|)) . T))
((($) . T))
((((-566) |#1|) . T))
@@ -2373,7 +2373,7 @@
((($) -2805 (|has| |#1| (-365)) (|has| |#1| (-351))) (((-409 (-566))) -2805 (|has| |#1| (-365)) (|has| |#1| (-351))) ((|#1|) . T))
((((-566)) . T))
(|has| |#1| (-38 (-409 (-566))))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 (-52))))))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 (-52))))))
(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))))
(|has| |#1| (-848))
(|has| |#1| (-38 (-409 (-566))))
@@ -2416,10 +2416,10 @@
((($) -2805 (|has| |#1| (-172)) (|has| |#1| (-365)) (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) ((|#1|) . T) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))))
((((-538)) |has| |#4| (-614 (-538))))
((((-862)) . T) (((-644 |#4|)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#1|) . T))
(|has| |#1| (-848))
-(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) (((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)))))
+(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) (((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)))))
(|has| |#1| (-1099))
(|has| |#1| (-365))
(((|#1|) . T))
@@ -2464,7 +2464,7 @@
((((-862)) . T))
((((-862)) . T))
((((-538)) |has| |#1| (-614 (-538))))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-566)) . T) (($) . T) (((-409 (-566))) . T))
((((-1175) |#1|) |has| |#1| (-516 (-1175) |#1|)) ((|#1| |#1|) |has| |#1| (-310 |#1|)))
(((|#1|) -2805 (|has| |#1| (-172)) (|has| |#1| (-365))))
@@ -2503,7 +2503,7 @@
(|has| |#1| (-558))
(((|#2|) . T))
((((-566)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#1|) . T))
(-2805 (|has| |#1| (-145)) (|has| |#1| (-147)) (|has| |#1| (-172)) (|has| |#1| (-558)) (|has| |#1| (-1049)))
(((|#1| (-59 |#1|) (-59 |#1|)) . T))
@@ -2514,7 +2514,7 @@
((($) . T))
(((|#1|) . T))
((((-862)) . T))
-(((|#2|) |has| |#2| (-6 (-4419 "*"))))
+(((|#2|) |has| |#2| (-6 (-4416 "*"))))
(((|#1|) . T))
(((|#1|) . T))
((($) . T))
@@ -2636,22 +2636,22 @@
(((|#2|) . T))
(((|#4| |#4|) -12 (|has| |#4| (-310 |#4|)) (|has| |#4| (-1099))))
(((|#2|) . T))
-(((|#2|) -2805 (|has| |#2| (-6 (-4419 "*"))) (|has| |#2| (-172))))
+(((|#2|) -2805 (|has| |#2| (-6 (-4416 "*"))) (|has| |#2| (-172))))
(-2805 (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909)))
(-2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909)))
(|has| |#2| (-909))
(|has| |#1| (-909))
(((|#2|) |has| |#2| (-172)))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-1256 |#1| |#2| |#3|)) |has| |#1| (-365)))
((((-862)) . T))
((((-862)) . T))
((((-538)) . T) (((-566)) . T) (((-892 (-566))) . T) (((-381)) . T) (((-225)) . T))
(((|#1| |#2|) . T))
((($) . T) (((-566)) . T))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) . T))
(((|#1|) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-862)) . T))
(((|#1| |#2|) . T))
((($) . T) (((-566)) . T))
@@ -2673,7 +2673,7 @@
((((-862)) . T))
((((-862)) . T))
((((-187)) . T) (((-862)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#2| |#2|) . T) ((|#1| |#1|) . T))
((((-862)) . T))
((((-862)) . T))
@@ -2686,7 +2686,7 @@
((((-862)) . T))
((((-1157)) . T))
((((-1175) |#1|) |has| |#1| (-516 (-1175) |#1|)) ((|#1| |#1|) |has| |#1| (-310 |#1|)))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
(|has| |#1| (-850))
((((-862)) . T))
((((-538)) |has| |#1| (-614 (-538))))
@@ -2748,8 +2748,8 @@
(-2805 (|has| |#1| (-145)) (|has| |#1| (-370)))
(-2805 (|has| |#1| (-145)) (|has| |#1| (-370)))
(-2805 (|has| |#1| (-145)) (|has| |#1| (-370)))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T))
-(((#0=(-52)) . T) (((-2 (|:| -2010 (-1175)) (|:| -2818 #0#))) . T))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T))
+(((#0=(-52)) . T) (((-2 (|:| -2050 (-1175)) (|:| -2849 #0#))) . T))
(|has| |#1| (-351))
((((-566)) . T))
((((-862)) . T))
@@ -2835,7 +2835,7 @@
(|has| |#2| (-1022))
((($) . T))
(|has| |#1| (-909))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((($) . T))
(((|#2|) . T))
(((|#1|) . T))
@@ -2858,12 +2858,12 @@
((((-566)) . T) (($) . T))
((((-566)) . T) (($) . T))
((((-771) |#1|) . T))
-(((|#2| (-240 (-2997 |#1|) (-771))) . T))
+(((|#2| (-240 (-3020 |#1|) (-771))) . T))
(((|#1| (-533 |#3|)) . T))
((((-409 (-566))) . T))
(-2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909)))
((((-1157)) . T) (((-862)) . T))
-(((#0=(-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) #0#) |has| (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))))))
+(((#0=(-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) #0#) |has| (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))))))
((((-1157)) . T))
(|has| |#1| (-909))
(|has| |#2| (-365))
@@ -2901,7 +2901,7 @@
(((|#2|) |has| |#1| (-365)))
(((|#2|) |has| |#1| (-365)))
((((-566)) . T) (($) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#1|) . T))
(((|#1|) |has| |#1| (-172)))
(((|#1|) . T))
@@ -2947,9 +2947,9 @@
(((|#2|) . T))
(((|#2|) . T))
(-2805 (|has| |#2| (-172)) (|has| |#2| (-726)) (|has| |#2| (-848)) (|has| |#2| (-1049)))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(|has| |#1| (-38 (-409 (-566))))
(((|#1| |#2|) . T))
(|has| |#1| (-38 (-409 (-566))))
@@ -3081,7 +3081,7 @@
(|has| |#2| (-365))
((((-583 |#1|)) . T) (((-409 (-566))) . T) (($) . T) (((-566)) . T))
((((-566)) . T) (((-409 (-566))) . T) (($) . T))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) . T))
(((|#1|) . T))
(((|#1|) . T) (((-566)) . T))
(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))))
@@ -3115,7 +3115,7 @@
(((|#1|) . T))
(((|#1|) . T))
((($) . T) (((-409 (-566))) . T))
-(((|#2|) |has| |#2| (-6 (-4419 "*"))))
+(((|#2|) |has| |#2| (-6 (-4416 "*"))))
(((|#1|) . T))
((((-409 (-566))) |has| |#1| (-1038 (-409 (-566)))) ((|#1|) . T) (((-566)) . T))
(((|#1|) . T))
@@ -3143,7 +3143,7 @@
((($) -2805 (|has| |#1| (-172)) (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) ((|#1|) . T) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))))
((((-862)) . T))
(((|#1|) . T))
-((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T))
+((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T))
(((|#1|) . T))
(((|#1|) . T))
(((|#1|) . T))
@@ -3228,7 +3228,7 @@
(((|#1|) . T))
(((|#1|) |has| |#1| (-172)))
(((|#4|) -12 (|has| |#4| (-310 |#4|)) (|has| |#4| (-1099))))
-(((|#2|) -2805 (|has| |#2| (-6 (-4419 "*"))) (|has| |#2| (-172))))
+(((|#2|) -2805 (|has| |#2| (-6 (-4416 "*"))) (|has| |#2| (-172))))
(((|#2|) . T))
(|has| |#1| (-365))
(((|#2|) . T))
@@ -3274,7 +3274,7 @@
(((|#1|) . T))
((((-862)) . T))
(|has| |#2| (-909))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T))
((((-538)) |has| |#2| (-614 (-538))) (((-892 (-381))) |has| |#2| (-614 (-892 (-381)))) (((-892 (-566))) |has| |#2| (-614 (-892 (-566)))))
((((-862)) . T))
((((-862)) . T))
@@ -3317,7 +3317,7 @@
((((-409 |#2|) |#3|) . T))
(((|#1|) . T))
(|has| |#1| (-1099))
-(((|#2| (-484 (-2997 |#1|) (-771))) . T))
+(((|#2| (-484 (-3020 |#1|) (-771))) . T))
((((-566) |#1|) . T))
((((-1157)) . T) (((-862)) . T))
(((|#2| |#2|) . T))
@@ -3376,7 +3376,7 @@
((((-1175)) -12 (|has| |#3| (-900 (-1175))) (|has| |#3| (-1049))))
(((|#1|) . T))
(|has| |#1| (-233))
-(((|#2| (-240 (-2997 |#1|) (-771))) . T))
+(((|#2| (-240 (-3020 |#1|) (-771))) . T))
(((|#1| (-533 |#3|)) . T))
(|has| |#1| (-370))
(|has| |#1| (-370))
@@ -3465,7 +3465,7 @@
((((-1213)) . T) (((-862)) . T) (((-1180)) . T))
((((-1180)) . T))
((((-1180)) . T))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) |has| (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))))))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) |has| (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))))))
(-2805 (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909)))
((((-566) |#1|) . T))
((((-566) |#1|) . T))
@@ -3672,7 +3672,7 @@
(-2805 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-131)) (|has| |#2| (-131))) (-12 (|has| |#1| (-793)) (|has| |#2| (-793))))
((((-566)) . T))
((((-566)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(((|#1| |#2|) . T))
(((|#1|) . T))
(-2805 (|has| |#2| (-172)) (|has| |#2| (-726)) (|has| |#2| (-848)) (|has| |#2| (-1049)))
@@ -3779,11 +3779,11 @@
((((-1173 |#1| |#2| |#3|)) |has| |#1| (-365)))
((((-1139 |#1| |#2|)) . T))
((((-1173 |#1| |#2| |#3|)) |has| |#1| (-365)))
-(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T))
+(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T))
((($) . T))
(|has| |#1| (-1022))
-(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
((((-862)) . T))
((((-538)) |has| |#2| (-614 (-538))) (((-892 (-566))) |has| |#2| (-614 (-892 (-566)))) (((-892 (-381))) |has| |#2| (-614 (-892 (-381)))) (((-381)) . #0=(|has| |#2| (-1022))) (((-225)) . #0#))
((((-295 |#3|)) . T))
@@ -3838,7 +3838,7 @@
((((-862)) . T))
((((-862)) . T))
(((|#1| (-533 |#2|)) . T))
-((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T))
+((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T))
((((-566) (-129)) . T))
(((|#1| (-566)) . T))
(((|#1| (-409 (-566))) . T))
@@ -3875,7 +3875,7 @@
(((|#1| |#2|) . T))
((((-1157) |#1|) . T))
((((-409 |#2|)) . T))
-((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T))
+((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T))
(|has| |#1| (-558))
(|has| |#1| (-558))
((($) . T) ((|#2|) . T))
@@ -3909,7 +3909,7 @@
(((|#1| |#2| |#3| |#4|) . T))
(((#0=(-1139 |#1| |#2|) #0#) |has| (-1139 |#1| |#2|) (-310 (-1139 |#1| |#2|))))
(((|#1|) . T))
-(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))))
(((#0=(-116 |#1|)) |has| #0# (-310 #0#)))
((($ $) . T))
(-2805 (|has| |#1| (-850)) (|has| |#1| (-1099)))