:: GOBOARD4  semantic presentation begin  

































theorem :: GOBOARD4:1 (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")))) & (Bool (Set (Var "f1"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "f2"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )))) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f1")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f2")))))) ; 
 
theorem :: GOBOARD4:2 (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")))) & (Bool (Set (Var "f1"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "f2"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f1")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f2")))))) ; 
 
theorem :: GOBOARD4:3 (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")))) & (Bool (Set (Var "f1"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "f2"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f1")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f2")))))) ; 
 definitionlet "f" be   ($#m1_hidden :::"Relation":::); let "r", "s" be   ($#m1_subset_1 :::"Real":::); pred "f" :::"lies_between"::: "r" "," "s" means :: GOBOARD4:def 1 (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  "f")  ($#r1_tarski :::"c="::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) "r" "," "s" ($#k1_xxreal_1 :::".]"::: ) )); end; 






:: deftheorem    defines :::"lies_between"::: GOBOARD4:def 1 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Var "r")) "," (Set (Var "s"))) "iff" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_xxreal_1 :::".]"::: ) ))  ")" ))); 
 definitionlet "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); let "r", "s" be   ($#m1_subset_1 :::"Real":::); redefine pred "f" :::"lies_between"::: "r" "," "s" means :: GOBOARD4:def 2 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "f"))) "holds"  (Bool  "("  (Bool "r"  ($#r1_xxreal_0 :::"<="::: )  (Set "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  "s")  ")" )); end; 






:: deftheorem    defines :::"lies_between"::: GOBOARD4:def 2 :  (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Var "r")) "," (Set (Var "s"))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  ")" ))  ")" ))); 
 
theorem :: GOBOARD4:4 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")))) & (Bool (Set (Var "f1")) "is"   ($#v1_topreal1 :::"special"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_topreal1 :::"special"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f1")))) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f2")))) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f2"))))) "holds"  (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" ) & (Bool (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")) ")" )  ($#k1_seq_1 :::"."::: )  (Num 1)) "," (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))) & (Bool (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f2")))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")) ")" )  ($#k1_seq_1 :::"."::: )  (Num 1)) "," (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))) & (Bool (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f1")))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Num 1)) "," (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Num 1)) "," (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")) ")" )))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f1")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f2"))))) ; 
 
theorem :: GOBOARD4:5 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "f1")) "is"   ($#v1_topreal1 :::"special"::: )  ) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Set (Var "f2")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_topreal1 :::"special"::: )  ) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")))) & (Bool (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")) ")" )  ($#k1_seq_1 :::"."::: )  (Num 1)) "," (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))) & (Bool (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f2")))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")) ")" )  ($#k1_seq_1 :::"."::: )  (Num 1)) "," (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))) & (Bool (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f1")))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Num 1)) "," (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")))  ($#r1_goboard4 :::"lies_between"::: )  (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Num 1)) "," (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")) ")" )))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f1")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f2"))))) ; 
 
theorem :: GOBOARD4:6 (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P1"))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Var "p1")) "," (Set (Var "q1"))) & (Bool (Set (Var "P2"))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Var "p2")) "," (Set (Var "q2"))) & (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "P1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "P2"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  ))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "P1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "P2"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  ))  ")" )  ")" )) "holds"  (Bool (Set (Var "P1"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "P2"))))) ;