:: GOBRD10  semantic presentation begin  















definitionlet "i1", "i2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); pred "i1" "," "i2" :::"are_adjacent1":::  means :: GOBRD10:def 1 (Bool  "("  (Bool "i2"  ($#r1_hidden :::"="::: )  (Set "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1))) "or" (Bool "i1"  ($#r1_hidden :::"="::: )  (Set "i2"  ($#k2_nat_1 :::"+"::: )  (Num 1)))  ")" ); symmetry  
(Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("  (Bool  "("  (Bool (Bool  "not" (Set (Var "i2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))) & (Bool (Bool  "not" (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))))  ")" ) "or" (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) "or" (Bool (Set (Var "i2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))  ")" ))
 ; irreflexivity  
(Bool  "for" (Set (Var "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))) & (Bool (Bool  "not" (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))))  ")" ))
 ; end; 





:: deftheorem    defines :::"are_adjacent1"::: GOBRD10:def 1 :  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r1_gobrd10 :::"are_adjacent1"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "i2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) "or" (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))  ")" )  ")" )); 
 
theorem :: GOBRD10:1 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r1_gobrd10 :::"are_adjacent1"::: )  )) "holds"  (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1)) "," (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_gobrd10 :::"are_adjacent1"::: )  )) ; 
 
theorem :: GOBRD10:2 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r1_gobrd10 :::"are_adjacent1"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2")))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Num 1)) "," (Set (Set (Var "i2"))  ($#k7_nat_d :::"-'"::: )  (Num 1))  ($#r1_gobrd10 :::"are_adjacent1"::: )  )) ; 
 definitionlet "i1", "j1", "i2", "j2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); pred "i1" "," "j1" "," "i2" "," "j2" :::"are_adjacent2":::  means :: GOBRD10:def 2 (Bool  "("  (Bool  "("  (Bool "i1" "," "i2"  ($#r1_gobrd10 :::"are_adjacent1"::: )  ) & (Bool "j1"  ($#r1_hidden :::"="::: )  "j2")  ")" ) "or" (Bool  "("  (Bool "i1"  ($#r1_hidden :::"="::: )  "i2") & (Bool "j1" "," "j2"  ($#r1_gobrd10 :::"are_adjacent1"::: )  )  ")" )  ")" ); end; 







:: deftheorem    defines :::"are_adjacent2"::: GOBRD10:def 2 :  (Bool  "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2"))  ($#r2_gobrd10 :::"are_adjacent2"::: )  ) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r1_gobrd10 :::"are_adjacent1"::: )  ) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "j1")) "," (Set (Var "j2"))  ($#r1_gobrd10 :::"are_adjacent1"::: )  )  ")" )  ")" )  ")" )); 
 
theorem :: GOBRD10:3 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "j1")) "," (Set (Var "j2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2"))  ($#r2_gobrd10 :::"are_adjacent2"::: )  )) "holds"  (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1)) "," (Set (Set (Var "j1"))  ($#k2_nat_1 :::"+"::: )  (Num 1)) "," (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1)) "," (Set (Set (Var "j2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_gobrd10 :::"are_adjacent2"::: )  )) ; 
 
theorem :: GOBRD10:4 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "j1")) "," (Set (Var "j2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2"))  ($#r2_gobrd10 :::"are_adjacent2"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j1"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j2")))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Num 1)) "," (Set (Set (Var "j1"))  ($#k7_nat_d :::"-'"::: )  (Num 1)) "," (Set (Set (Var "i2"))  ($#k7_nat_d :::"-'"::: )  (Num 1)) "," (Set (Set (Var "j2"))  ($#k7_nat_d :::"-'"::: )  (Num 1))  ($#r2_gobrd10 :::"are_adjacent2"::: )  )) ; 
 
theorem :: GOBRD10:5 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "fs1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "j"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "j"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "k")) "," (Set (Var "k1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")))) & (Bool (Set (Var "k1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))) "holds"  (Bool (Set (Var "k1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ) & (Bool  "("   "for" (Set (Var "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")))) & (Bool (Bool  "not" (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "fs1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))))) "holds"  (Bool (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "fs1"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))  ")" )  ")" ))) ; 
 
theorem :: GOBRD10:6 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "fs1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "j"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "j"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "k")) "," (Set (Var "k1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")))) & (Bool (Set (Var "k1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))) "holds"  (Bool (Set (Var "k1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ) & (Bool  "("   "for" (Set (Var "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1"))))) "holds"  (Bool (Set (Set (Var "fs1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1"))) "," (Set (Set (Var "fs1"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_gobrd10 :::"are_adjacent1"::: )  )  ")" )  ")" ))) ; 
 
theorem :: GOBRD10:7 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "j1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "j2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "ex" (Set (Var "fs1")) "," (Set (Var "fs2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "k1")) "," (Set (Var "k2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "fs1")))) & (Bool (Set (Var "k1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "k2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fs2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))) "holds"  (Bool  "("  (Bool (Set (Var "k1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "k2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))  ")" )  ")" ) & (Bool (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "i1"))) & (Bool (Set (Set (Var "fs1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "fs2"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "j1"))) & (Bool (Set (Set (Var "fs2"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs2")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "i2"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i1")) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "j1"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j2")) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "j2"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j1")) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs1"))))) "holds"  (Bool (Set (Set (Var "fs1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i"))) "," (Set (Set (Var "fs2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i"))) "," (Set (Set (Var "fs1"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )) "," (Set (Set (Var "fs2"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r2_gobrd10 :::"are_adjacent2"::: )  )  ")" )  ")" ))) ; 
 



theorem :: GOBRD10:8 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "S")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "being"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "S")))  "st" (Bool (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Set (Var "F"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" )) & (Bool  "("   "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "i2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "j1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "j2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2"))  ($#r2_gobrd10 :::"are_adjacent2"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) "iff" (Bool (Set (Set (Var "F"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))))))) ;