:: GOBOARD3  semantic presentation begin  

























theorem :: GOBOARD3:1 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_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  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "G")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ))  ")" ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_topreal1 :::"unfolded"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v3_topreal1 :::"s.n.c."::: )  ) & (Bool (Set (Var "f")) "is"   ($#v1_topreal1 :::"special"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "g"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_topreal1 :::"unfolded"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v3_topreal1 :::"s.n.c."::: )  ) & (Bool (Set (Var "g")) "is"   ($#v1_topreal1 :::"special"::: )  ) & (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Num 1))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g"))))  ")" )))) ; 
 
theorem :: GOBOARD3:2 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_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  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "G")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ))  ")" ) & (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "g"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "g")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Num 1))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g"))))  ")" )))) ;