-
Notifications
You must be signed in to change notification settings - Fork 10
/
Copy pathl10_jordan1d
27 lines (27 loc) · 13.9 KB
/
l10_jordan1d
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
C * ! / b0 * * c=> * cv1_xreal_0 b0 * * c=> * * cr1_xxreal_0 c1 b0 * * cr1_xxreal_0 ck6_numbers * * ck9_real_1 * * ck8_real_1 c2 b0 c1
+ * ! / b0 * * c=> * * cm1_subset_1 b0 ck1_numbers * cv1_xreal_0 b0
+ * ! / b0 * ! / b1 * * c=> * * c& * * cm1_subset_1 b0 ck1_numbers * cv1_xreal_0 b1 * * cm1_subset_1 * * ck8_real_1 b0 b1 ck1_numbers
+ * * c= ck6_numbers ck1_xboole_0
+ * ! / b0 * ! / b1 * * c=> * * c& * * cm1_subset_1 b0 ck1_numbers * cv1_xreal_0 b1 * * c= * * ck8_real_1 b0 b1 * * ck3_xcmplx_0 b0 b1
+ * ! / b0 * ! / b1 * * c=> * * c& * * cm1_subset_1 b0 ck1_numbers * cv1_xreal_0 b1 * * c= * * ck9_real_1 b0 b1 * * ck6_xcmplx_0 b0 b1
+ * * cr1_xxreal_0 c1 c2
+ * * c= * * ck6_xcmplx_0 c1 c1 c0
+ * cv1_xboole_0 c0
+ * * c& * * c& * cv2_xxreal_0 c1 * * * cm2_subset_1 c1 ck1_numbers ck5_numbers * * c& * * cm1_subset_1 c1 ck5_numbers * * cm1_subset_1 c1 ck1_numbers
+ * * c& * * c& * cv2_xxreal_0 c2 * * * cm2_subset_1 c2 ck1_numbers ck5_numbers * * c& * * cm1_subset_1 c2 ck5_numbers * * cm1_subset_1 c2 ck1_numbers
+ * ! / b0 * * c=> * cv1_xreal_0 b0 * ! / b1 * * c=> * cv1_xreal_0 b1 * * c=> * * c& * * cr1_xxreal_0 c1 b0 * * cr1_xxreal_0 c1 b1 * * cr1_xxreal_0 c1 * * ck3_xcmplx_0 b0 b1
+ * ! / b0 * * c=> * cv1_xboole_0 b0 * * c= b0 ck1_xboole_0
+ * ! / b0 * * c=> * cv1_xreal_0 b0 * ! / b1 * * c=> * cv1_xreal_0 b1 * ! / b2 * * c=> * cv1_xreal_0 b2 * * c<=> * * cr1_xxreal_0 b0 b1 * * cr1_xxreal_0 * * ck6_xcmplx_0 b0 b2 * * ck6_xcmplx_0 b1 b2
- * ! / b0 * * c=> * * cm1_subset_1 b0 * ck1_zfmisc_1 * cu1_struct_0 * * ck2_borsuk_1 ck5_topmetr ck5_topmetr * * c<=> * * c= b0 ck8_borsuk_6 * ! / b1 * * c<=> * * cr2_hidden b1 b0 * c? / b2 * * c& * * cm1_subset_1 b2 * cu1_struct_0 ck5_topmetr * c? / b3 * * c& * * cm1_subset_1 b3 * cu1_struct_0 ck5_topmetr * * c& * * c= b1 * * * * ck4_borsuk_1 ck5_topmetr ck5_topmetr b2 b3 * * cr1_xxreal_0 b3 * * ck9_real_1 * * ck8_real_1 c2 b2 c1
- * ! / b0 * * c<=> * * cr2_hidden b0 ca_0_14_borsuk_6 * c? / b1 * * c& * * cm1_subset_1 b1 * cu1_struct_0 * * ck2_borsuk_1 ck5_topmetr ck5_topmetr * * c& * * c= b0 b1 * * cr1_xxreal_0 * ck2_xtuple_0 b1 * * ck9_real_1 * * ck8_real_1 c2 * ck1_xtuple_0 b1 c1
- * ! / b0 * * c<=> * * cr2_hidden b0 ca_0_0_borsuk_6 * c? / b1 * * c& * * cm1_subset_1 b1 * cu1_struct_0 * ck15_euclid c2 * * c& * * c= b0 b1 * * cr1_xxreal_0 * ck18_euclid b1 * * ck9_real_1 * * ck8_real_1 c2 * ck17_euclid b1 c1
- * ! / b0 * * c<=> * * cr2_hidden b0 ca_0_10_borsuk_6 * c? / b1 * * c& * * cm1_subset_1 b1 * cu1_struct_0 * * ck2_borsuk_1 ck3_topmetr ck3_topmetr * * c& * * c= b0 b1 * * cr1_xxreal_0 * ck2_xtuple_0 b1 * * ck9_real_1 * * ck8_real_1 c2 * ck1_xtuple_0 b1 c1
- * ! / b0 * * c=> * * cm1_subset_1 b0 * ck1_zfmisc_1 * cu1_struct_0 * * ck2_borsuk_1 ck5_topmetr ck5_topmetr * * c<=> * * c= b0 ck7_borsuk_6 * ! / b1 * * c<=> * * cr2_hidden b1 b0 * c? / b2 * * c& * * cm1_subset_1 b2 * cu1_struct_0 ck5_topmetr * c? / b3 * * c& * * cm1_subset_1 b3 * cu1_struct_0 ck5_topmetr * * c& * * c= b1 * * * * ck4_borsuk_1 ck5_topmetr ck5_topmetr b2 b3 * * c& * * cr1_xxreal_0 * * ck9_real_1 c1 * * ck8_real_1 c2 b2 b3 * * cr1_xxreal_0 * * ck9_real_1 * * ck8_real_1 c2 b2 c1 b3
- * ! / b0 * * c<=> * * cr2_hidden b0 ca_0_8_borsuk_6 * c? / b1 * * c& * * cm1_subset_1 b1 * cu1_struct_0 * ck15_euclid c2 * * c& * * c= b0 b1 * * c& * * cr1_xxreal_0 * * ck9_real_1 c1 * * ck8_real_1 c2 * ck17_euclid b1 * ck18_euclid b1 * * cr1_xxreal_0 * * ck9_real_1 * * ck8_real_1 c2 * ck17_euclid b1 c1 * ck18_euclid b1
- * ! / b0 * * c<=> * * cr2_hidden b0 ca_0_11_borsuk_6 * c? / b1 * * c& * * cm1_subset_1 b1 * cu1_struct_0 * * ck2_borsuk_1 ck3_topmetr ck3_topmetr * * c& * * c= b0 b1 * * c& * * cr1_xxreal_0 * * ck9_real_1 c1 * * ck8_real_1 c2 * ck1_xtuple_0 b1 * ck2_xtuple_0 b1 * * cr1_xxreal_0 * * ck9_real_1 * * ck8_real_1 c2 * ck1_xtuple_0 b1 c1 * ck2_xtuple_0 b1
- * ! / b0 * * c<=> * * cr2_hidden b0 ca_0_13_borsuk_6 * c? / b1 * * c& * * cm1_subset_1 b1 * cu1_struct_0 * * ck2_borsuk_1 ck5_topmetr ck5_topmetr * * c& * * c= b0 b1 * * c& * * cr1_xxreal_0 * * ck9_real_1 c1 * * ck8_real_1 c2 * ck1_xtuple_0 b1 * ck2_xtuple_0 b1 * * cr1_xxreal_0 * * ck9_real_1 * * ck8_real_1 c2 * ck1_xtuple_0 b1 c1 * ck2_xtuple_0 b1
- * ! / b0 * * c<=> * * cr2_hidden b0 ca_0_2_borsuk_6 * c? / b1 * * c& * * cm1_subset_1 b1 * cu1_struct_0 * ck15_euclid c2 * * c& * * c= b0 b1 * * cr1_xxreal_0 * * ck9_real_1 * * ck8_real_1 c2 * ck17_euclid b1 c1 * ck18_euclid b1
- * ! / b0 * * c=> * cv1_xreal_0 b0 * ! / b1 * * c=> * cv1_xreal_0 b1 * ! / b2 * * c=> * cv1_xreal_0 b2 * ! / b3 * * c=> * cv1_xreal_0 b3 * c~ * * c& * c~ * * cr1_xxreal_0 b1 b0 * * c& * c~ * * cr1_xxreal_0 b3 b2 * ! / b4 * * c=> * * c& * cv1_funct_1 b4 * * c& * * * cv1_funct_2 b4 * cu1_struct_0 ck5_topmetr * cu1_struct_0 * * ck1_pre_topc * ck15_euclid c2 * ck9_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 * * cm1_subset_1 b4 * ck1_zfmisc_1 * * ck2_zfmisc_1 * cu1_struct_0 ck5_topmetr * cu1_struct_0 * * ck1_pre_topc * ck15_euclid c2 * ck9_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 * c~ * * c& * * * cv3_tops_2 b4 ck5_topmetr * * ck1_pre_topc * ck15_euclid c2 * ck9_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 * * c& * * c= * * ck1_funct_1 b4 ck6_numbers * ck22_pscomp_1 * * * * ck1_sppol_2 b0 b1 b2 b3 * * c& * * c= * * ck1_funct_1 b4 c1 * ck18_pscomp_1 * * * * ck1_sppol_2 b0 b1 b2 b3 * * c& * * c= * * ck2_relset_1 * cu1_struct_0 * * ck1_pre_topc * ck15_euclid c2 * ck9_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 b4 * ck9_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 * * c& * ! / b5 * * c=> * * cm1_subset_1 b5 ck1_numbers * * c=> * * cr2_hidden b5 * * ck1_rcomp_1 ck6_numbers * * ck10_real_1 c1 c2 * * c= * * ck1_funct_1 b4 b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b3 * * ck9_real_1 c1 * * ck8_real_1 c2 b5 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b2 * * ck8_real_1 c2 b5 * * c& * ! / b5 * * c=> * * cm1_subset_1 b5 ck1_numbers * * c=> * * cr2_hidden b5 * * ck1_rcomp_1 * * ck10_real_1 c1 c2 c1 * * c= * * ck1_funct_1 b4 b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b2 * * ck9_real_1 c1 * * ck9_real_1 * * ck8_real_1 c2 b5 c1 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b2 * * ck9_real_1 * * ck8_real_1 c2 b5 c1 * * c& * ! / b5 * * c=> * * cm1_subset_1 b5 * cu1_struct_0 * ck15_euclid c2 * * c=> * * cr2_hidden b5 * * * ck1_rltopsp1 * ck15_euclid c2 * * ck19_euclid b1 b3 * * ck19_euclid b1 b2 * * c& * * cr1_xxreal_0 ck6_numbers * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck18_euclid b5 b3 * * ck6_xcmplx_0 b2 b3 c2 * * c& * * cr1_xxreal_0 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck18_euclid b5 b3 * * ck6_xcmplx_0 b2 b3 c2 c1 * * c= * * ck1_funct_1 b4 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck18_euclid b5 b3 * * ck6_xcmplx_0 b2 b3 c2 b5 * ! / b5 * * c=> * * cm1_subset_1 b5 * cu1_struct_0 * ck15_euclid c2 * * c=> * * cr2_hidden b5 * * * ck1_rltopsp1 * ck15_euclid c2 * * ck19_euclid b1 b2 * * ck19_euclid b0 b2 * * c& * * cr1_xxreal_0 ck6_numbers * * ck7_real_1 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck17_euclid b5 b1 * * ck6_xcmplx_0 b0 b1 c2 * * ck10_real_1 c1 c2 * * c& * * cr1_xxreal_0 * * ck7_real_1 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck17_euclid b5 b1 * * ck6_xcmplx_0 b0 b1 c2 * * ck10_real_1 c1 c2 c1 * * c= * * ck1_funct_1 b4 * * ck7_real_1 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck17_euclid b5 b1 * * ck6_xcmplx_0 b0 b1 c2 * * ck10_real_1 c1 c2 b5
- * ! / b0 * * c=> * cv1_xreal_0 b0 * ! / b1 * * c=> * cv1_xreal_0 b1 * ! / b2 * * c=> * cv1_xreal_0 b2 * ! / b3 * * c=> * cv1_xreal_0 b3 * c~ * * c& * c~ * * cr1_xxreal_0 b1 b0 * * c& * c~ * * cr1_xxreal_0 b3 b2 * ! / b4 * * c=> * * c& * cv1_funct_1 b4 * * c& * * * cv1_funct_2 b4 * cu1_struct_0 ck5_topmetr * cu1_struct_0 * * ck1_pre_topc * ck15_euclid c2 * ck8_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 * * cm1_subset_1 b4 * ck1_zfmisc_1 * * ck2_zfmisc_1 * cu1_struct_0 ck5_topmetr * cu1_struct_0 * * ck1_pre_topc * ck15_euclid c2 * ck8_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 * c~ * * c& * * * cv3_tops_2 b4 ck5_topmetr * * ck1_pre_topc * ck15_euclid c2 * ck8_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 * * c& * * c= * * ck1_funct_1 b4 ck6_numbers * ck18_pscomp_1 * * * * ck1_sppol_2 b0 b1 b2 b3 * * c& * * c= * * ck1_funct_1 b4 c1 * ck22_pscomp_1 * * * * ck1_sppol_2 b0 b1 b2 b3 * * c& * * c= * * ck2_relset_1 * cu1_struct_0 * * ck1_pre_topc * ck15_euclid c2 * ck8_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 b4 * ck8_jordan6 * * * * ck1_sppol_2 b0 b1 b2 b3 * * c& * ! / b5 * * c=> * * cm1_subset_1 b5 ck1_numbers * * c=> * * cr2_hidden b5 * * ck1_rcomp_1 ck6_numbers * * ck10_real_1 c1 c2 * * c= * * ck1_funct_1 b4 b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b2 * * ck9_real_1 c1 * * ck8_real_1 c2 b5 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b3 * * ck8_real_1 c2 b5 * * c& * ! / b5 * * c=> * * cm1_subset_1 b5 ck1_numbers * * c=> * * cr2_hidden b5 * * ck1_rcomp_1 * * ck10_real_1 c1 c2 c1 * * c= * * ck1_funct_1 b4 b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b3 * * ck9_real_1 c1 * * ck9_real_1 * * ck8_real_1 c2 b5 c1 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b3 * * ck9_real_1 * * ck8_real_1 c2 b5 c1 * * c& * ! / b5 * * c=> * * cm1_subset_1 b5 * cu1_struct_0 * ck15_euclid c2 * * c=> * * cr2_hidden b5 * * * ck1_rltopsp1 * ck15_euclid c2 * * ck19_euclid b0 b2 * * ck19_euclid b0 b3 * * c& * * cr1_xxreal_0 ck6_numbers * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck18_euclid b5 b2 * * ck6_xcmplx_0 b3 b2 c2 * * c& * * cr1_xxreal_0 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck18_euclid b5 b2 * * ck6_xcmplx_0 b3 b2 c2 c1 * * c= * * ck1_funct_1 b4 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck18_euclid b5 b2 * * ck6_xcmplx_0 b3 b2 c2 b5 * ! / b5 * * c=> * * cm1_subset_1 b5 * cu1_struct_0 * ck15_euclid c2 * * c=> * * cr2_hidden b5 * * * ck1_rltopsp1 * ck15_euclid c2 * * ck19_euclid b0 b3 * * ck19_euclid b1 b3 * * c& * * cr1_xxreal_0 ck6_numbers * * ck7_real_1 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck17_euclid b5 b0 * * ck6_xcmplx_0 b1 b0 c2 * * ck10_real_1 c1 c2 * * c& * * cr1_xxreal_0 * * ck7_real_1 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck17_euclid b5 b0 * * ck6_xcmplx_0 b1 b0 c2 * * ck10_real_1 c1 c2 c1 * * c= * * ck1_funct_1 b4 * * ck7_real_1 * * ck10_real_1 * * ck10_real_1 * * ck9_real_1 * ck17_euclid b5 b0 * * ck6_xcmplx_0 b1 b0 c2 * * ck10_real_1 c1 c2 b5
- * ! / b0 * ! / b1 * ! / b2 * ! / b3 * * c=> * * c& * cv1_xreal_0 b0 * * c& * cv1_xreal_0 b1 * * c& * cv1_xreal_0 b2 * cv1_xreal_0 b3 * * c=> * ! / b4 * c~ * * c& * * cr2_hidden b4 * * ck1_rcomp_1 ck6_numbers c1 * ! / b5 * c~ * ! / b6 * * c=> * * cm1_subset_1 b6 ck1_numbers * * c=> * * c= b4 b6 * * c& * * c=> * * cr2_hidden b6 * * ck1_rcomp_1 ck6_numbers * * ck10_real_1 c1 c2 * * c= b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b2 * * ck9_real_1 c1 * * ck8_real_1 c2 b6 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b3 * * ck8_real_1 c2 b6 * * c=> * * cr2_hidden b6 * * ck1_rcomp_1 * * ck10_real_1 c1 c2 c1 * * c= b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b3 * * ck9_real_1 c1 * * ck9_real_1 * * ck8_real_1 c2 b6 c1 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b3 * * ck9_real_1 * * ck8_real_1 c2 b6 c1 * c? / b4 * * c& * * c& * cv1_relat_1 b4 * cv1_funct_1 b4 * * c& * * c= * ck9_xtuple_0 b4 * * ck1_rcomp_1 ck6_numbers c1 * ! / b5 * * c=> * * cr2_hidden b5 * * ck1_rcomp_1 ck6_numbers c1 * ! / b7 * * c=> * * cm1_subset_1 b7 ck1_numbers * * c=> * * c= b5 b7 * * c& * * c=> * * cr2_hidden b7 * * ck1_rcomp_1 ck6_numbers * * ck10_real_1 c1 c2 * * c= * * ck1_funct_1 b4 b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b2 * * ck9_real_1 c1 * * ck8_real_1 c2 b7 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b3 * * ck8_real_1 c2 b7 * * c=> * * cr2_hidden b7 * * ck1_rcomp_1 * * ck10_real_1 c1 c2 c1 * * c= * * ck1_funct_1 b4 b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b3 * * ck9_real_1 c1 * * ck9_real_1 * * ck8_real_1 c2 b7 c1 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b3 * * ck9_real_1 * * ck8_real_1 c2 b7 c1
- * ! / b0 * ! / b1 * ! / b2 * ! / b3 * * c=> * * c& * cv1_xreal_0 b0 * * c& * cv1_xreal_0 b1 * * c& * cv1_xreal_0 b2 * cv1_xreal_0 b3 * * c=> * ! / b4 * c~ * * c& * * cr2_hidden b4 * * ck1_rcomp_1 ck6_numbers c1 * ! / b5 * c~ * ! / b6 * * c=> * * cm1_subset_1 b6 ck1_numbers * * c=> * * c= b4 b6 * * c& * * c=> * * cr2_hidden b6 * * ck1_rcomp_1 ck6_numbers * * ck10_real_1 c1 c2 * * c= b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b3 * * ck9_real_1 c1 * * ck8_real_1 c2 b6 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b2 * * ck8_real_1 c2 b6 * * c=> * * cr2_hidden b6 * * ck1_rcomp_1 * * ck10_real_1 c1 c2 c1 * * c= b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b2 * * ck9_real_1 c1 * * ck9_real_1 * * ck8_real_1 c2 b6 c1 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b2 * * ck9_real_1 * * ck8_real_1 c2 b6 c1 * c? / b4 * * c& * * c& * cv1_relat_1 b4 * cv1_funct_1 b4 * * c& * * c= * ck9_xtuple_0 b4 * * ck1_rcomp_1 ck6_numbers c1 * ! / b5 * * c=> * * cr2_hidden b5 * * ck1_rcomp_1 ck6_numbers c1 * ! / b7 * * c=> * * cm1_subset_1 b7 ck1_numbers * * c=> * * c= b5 b7 * * c& * * c=> * * cr2_hidden b7 * * ck1_rcomp_1 ck6_numbers * * ck10_real_1 c1 c2 * * c= * * ck1_funct_1 b4 b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b3 * * ck9_real_1 c1 * * ck8_real_1 c2 b7 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b2 * * ck8_real_1 c2 b7 * * c=> * * cr2_hidden b7 * * ck1_rcomp_1 * * ck10_real_1 c1 c2 c1 * * c= * * ck1_funct_1 b4 b5 * * * ck3_rlvect_1 * ck15_euclid c2 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b1 b2 * * ck9_real_1 c1 * * ck9_real_1 * * ck8_real_1 c2 b7 c1 * * * ck1_rlvect_1 * ck15_euclid c2 * * ck19_euclid b0 b2 * * ck9_real_1 * * ck8_real_1 c2 b7 c1