:: EUCLIDLP semantic presentation begin theorem :: EUCLIDLP:1 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "s")) ($#k10_real_1 :::"/"::: ) (Set (Var "t")) ")" ) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "u")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "t")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "t")) ")" ) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "u")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "u")) ($#k10_real_1 :::"/"::: ) (Set (Var "t")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x")))) ")" )))) ; theorem :: EUCLIDLP:2 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" ))) ; theorem :: EUCLIDLP:3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set ($#k6_euclid :::"-"::: ) (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x")))) & (Bool (Set ($#k6_euclid :::"-"::: ) (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "x")) ")" ))) ")" )))) ; theorem :: EUCLIDLP:4 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "x3")))))) ; theorem :: EUCLIDLP:5 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k8_euclid :::"-"::: ) (Set (Var "x3")))))) ; theorem :: EUCLIDLP:6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k7_euclid :::"+"::: ) (Set (Var "x3")))) "iff" (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x3")))) ")" ))) ; theorem :: EUCLIDLP:7 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "x3")))) "iff" (Bool (Set (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k7_euclid :::"+"::: ) (Set (Var "x3")))) ")" ))) ; theorem :: EUCLIDLP:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k6_euclid :::"-"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "x3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "x3")) ")" ))))) ; theorem :: EUCLIDLP:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) "iff" (Bool (Set (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" ))) ; theorem :: EUCLIDLP:10 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x0")) "," (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x0"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k9_euclid :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x0")))) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: EUCLIDLP:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "b")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "b")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "b")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set "(" (Set (Var "b")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "b")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "b")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ))) ")" )))) ; theorem :: EUCLIDLP:12 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" ) ")" ))) & (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" ))) ")" )))) ; theorem :: EUCLIDLP:13 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "s")) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "u")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "s")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "t")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "u")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" )))))) ; theorem :: EUCLIDLP:14 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "a1")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "a2")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "a3")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ) ")" )))))) ; theorem :: EUCLIDLP:15 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set (Var "t")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "u")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "s")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "u")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" )))))) ; theorem :: EUCLIDLP:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "y1")) ($#k7_euclid :::"+"::: ) (Set (Var "y2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "y1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k7_euclid :::"+"::: ) (Set (Var "y2")) ")" ))))) ; theorem :: EUCLIDLP:17 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "x3")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "y1")) ($#k7_euclid :::"+"::: ) (Set (Var "y2")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "y3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "y1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k7_euclid :::"+"::: ) (Set (Var "y2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "x3")) ($#k7_euclid :::"+"::: ) (Set (Var "y3")) ")" ))))) ; theorem :: EUCLIDLP:18 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "y1")) ($#k7_euclid :::"+"::: ) (Set (Var "y2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "y2")) ")" ))))) ; theorem :: EUCLIDLP:19 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "x3")) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set "(" (Set (Var "y1")) ($#k7_euclid :::"+"::: ) (Set (Var "y2")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "y3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "y2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "y3")) ")" ))))) ; theorem :: EUCLIDLP:20 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "x3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" )))))) ; theorem :: EUCLIDLP:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set "(" (Set (Var "b1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b1")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b2")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )))))) ; theorem :: EUCLIDLP:22 (Bool "for" (Set (Var "a")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b1")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b2")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b3")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" )))))) ; theorem :: EUCLIDLP:23 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "b1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k7_real_1 :::"+"::: ) (Set (Var "b1")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k7_real_1 :::"+"::: ) (Set (Var "b2")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )))))) ; theorem :: EUCLIDLP:24 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k7_real_1 :::"+"::: ) (Set (Var "b1")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k7_real_1 :::"+"::: ) (Set (Var "b2")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "a3")) ($#k7_real_1 :::"+"::: ) (Set (Var "b3")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" )))))) ; theorem :: EUCLIDLP:25 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set "(" (Set (Var "b1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_real_1 :::"-"::: ) (Set (Var "b1")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k9_real_1 :::"-"::: ) (Set (Var "b2")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )))))) ; theorem :: EUCLIDLP:26 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k9_real_1 :::"-"::: ) (Set (Var "b1")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k9_real_1 :::"-"::: ) (Set (Var "b2")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "a3")) ($#k9_real_1 :::"-"::: ) (Set (Var "b3")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" )))))) ; theorem :: EUCLIDLP:27 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "a1")) ($#k7_real_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "a3"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ) ")" )))))) ; theorem :: EUCLIDLP:28 (Bool "for" (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ) ")" )))) "holds" (Bool "ex" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a1")) ($#k7_real_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "a3"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))))) ; theorem :: EUCLIDLP:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k21_euclid :::"1*"::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) ; theorem :: EUCLIDLP:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ))))) ; theorem :: EUCLIDLP:31 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" )))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x1", "x2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); pred "x1" :::"//"::: "x2" means :: EUCLIDLP:def 1 (Bool "(" (Bool "x1" ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) "n")) & (Bool "x2" ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) "n")) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "x1" ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) "x2"))) ")" ); end; :: deftheorem defines :::"//"::: EUCLIDLP:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_euclidlp :::"//"::: ) (Set (Var "x2"))) "iff" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "x2"))))) ")" ) ")" ))); theorem :: EUCLIDLP:32 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r1_euclidlp :::"//"::: ) (Set (Var "x2")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")))) ")" )))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x1", "x2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); :: original: :::"//"::: redefine pred "x1" :::"//"::: "x2"; symmetry (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))) "st" (Bool (Bool ((Set (Const "n")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "n")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: EUCLIDLP:33 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_euclidlp :::"//"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x2")) ($#r2_euclidlp :::"//"::: ) (Set (Var "x3")))) "holds" (Bool (Set (Var "x1")) ($#r2_euclidlp :::"//"::: ) (Set (Var "x3"))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x1", "x2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); pred "x1" "," "x2" :::"are_lindependent2"::: means :: EUCLIDLP:def 2 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) "x1" ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) "x2" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) "n"))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); symmetry (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))) "st" (Bool (Bool "(" "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Const "n"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Const "n"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; end; :: deftheorem defines :::"are_lindependent2"::: EUCLIDLP:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_euclidlp :::"are_lindependent2"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ))); notationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x1", "x2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); antonym "x1" "," "x2" :::"are_ldependent2"::: for "x1" "," "x2" :::"are_lindependent2"::: ; end; theorem :: EUCLIDLP:34 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_euclidlp :::"are_lindependent2"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" ))) ; theorem :: EUCLIDLP:35 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_euclidlp :::"are_lindependent2"::: ) ) & (Bool (Set (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )))) ; theorem :: EUCLIDLP:36 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y2")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "y1")) "," (Set (Var "y2")) ($#r3_euclidlp :::"are_lindependent2"::: ) ) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ))) & (Bool (Set (Var "y2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )))) "holds" (Bool "ex" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k9_euclid :::"*"::: ) (Set (Var "y1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k9_euclid :::"*"::: ) (Set (Var "y2")) ")" ))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "d1")) ($#k9_euclid :::"*"::: ) (Set (Var "y1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "d2")) ($#k9_euclid :::"*"::: ) (Set (Var "y2")) ")" ))) ")" ))))) ; theorem :: EUCLIDLP:37 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_euclidlp :::"are_lindependent2"::: ) )) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))))) ; theorem :: EUCLIDLP:38 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) "," (Set (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r3_euclidlp :::"are_lindependent2"::: ) )) "holds" (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))))) ; theorem :: EUCLIDLP:39 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_euclidlp :::"are_lindependent2"::: ) )) "holds" (Bool (Set (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "t")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )) "," (Set (Var "x2")) ($#r3_euclidlp :::"are_lindependent2"::: ) )))) ; theorem :: EUCLIDLP:40 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x0")) "," (Set (Var "x3")) "," (Set (Var "x2")) "," (Set (Var "y0")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x0"))) "," (Set (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x2"))) ($#r3_euclidlp :::"are_lindependent2"::: ) ) & (Bool (Set (Var "y0")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x0")) "," (Set (Var "x1")) ")" )) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x0")) "," (Set (Var "x1")) ")" )) & (Bool (Set (Var "y0")) ($#r1_hidden :::"<>"::: ) (Set (Var "y1"))) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set (Var "y3")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set (Var "y2")) ($#r1_hidden :::"<>"::: ) (Set (Var "y3")))) "holds" (Bool (Set (Set (Var "y1")) ($#k8_euclid :::"-"::: ) (Set (Var "y0"))) "," (Set (Set (Var "y3")) ($#k8_euclid :::"-"::: ) (Set (Var "y2"))) ($#r3_euclidlp :::"are_lindependent2"::: ) ))) ; theorem :: EUCLIDLP:41 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_euclidlp :::"//"::: ) (Set (Var "x2")))) "holds" (Bool "(" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_euclidlp :::"are_ldependent2"::: ) ) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" ))) ; theorem :: EUCLIDLP:42 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" "not" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_euclidlp :::"are_ldependent2"::: ) ) "or" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) "or" (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) "or" (Bool (Set (Var "x1")) ($#r2_euclidlp :::"//"::: ) (Set (Var "x2"))) ")" ))) ; theorem :: EUCLIDLP:43 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "ex" (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2"))) "," (Set (Set (Var "y1")) ($#k8_euclid :::"-"::: ) (Set (Var "y2"))) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ")" )))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x1", "x2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); pred "x1" :::"_|_"::: "x2" means :: EUCLIDLP:def 3 (Bool "(" (Bool "x1" ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) "n")) & (Bool "x2" ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) "n")) & (Bool "x1" "," "x2" ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ")" ); symmetry (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Const "n")))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Const "n")))) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Const "n")))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Const "n")))) & (Bool (Set (Var "x2")) "," (Set (Var "x1")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ")" )) ; end; :: deftheorem defines :::"_|_"::: EUCLIDLP:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r4_euclidlp :::"_|_"::: ) (Set (Var "x2"))) "iff" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ")" ) ")" ))); theorem :: EUCLIDLP:44 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r4_euclidlp :::"_|_"::: ) (Set (Var "y0"))) & (Bool (Set (Var "y0")) ($#r2_euclidlp :::"//"::: ) (Set (Var "y1")))) "holds" (Bool (Set (Var "x")) ($#r4_euclidlp :::"_|_"::: ) (Set (Var "y1"))))) ; theorem :: EUCLIDLP:45 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r4_euclidlp :::"_|_"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r3_euclidlp :::"are_lindependent2"::: ) ))) ; theorem :: EUCLIDLP:46 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_euclidlp :::"//"::: ) (Set (Var "x2")))) "holds" (Bool "not" (Bool (Set (Var "x1")) ($#r4_euclidlp :::"_|_"::: ) (Set (Var "x2")))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"line_of_REAL"::: "n" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) equals :: EUCLIDLP:def 4 "{" (Set "(" ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" ) where x1, x2 "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") : (Bool verum) "}" ; end; :: deftheorem defines :::"line_of_REAL"::: EUCLIDLP:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" ) where x1, x2 "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) : (Bool verum) "}" )); registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_euclidlp :::"line_of_REAL"::: ) "n") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: EUCLIDLP:47 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n")))))) ; theorem :: EUCLIDLP:48 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) "holds" (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "L")))))) ; theorem :: EUCLIDLP:49 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "L1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "L2"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L2"))) ")" )) ")" ))) ; theorem :: EUCLIDLP:50 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L0")) "," (Set (Var "L1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L0")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "L1"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L0")))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))))))) ; theorem :: EUCLIDLP:51 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ))))) ; theorem :: EUCLIDLP:52 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "ex" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))))) ; theorem :: EUCLIDLP:53 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x0"))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ))))) ; theorem :: EUCLIDLP:54 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r4_euclidlp :::"_|_"::: ) (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")))) ")" ))))) ; theorem :: EUCLIDLP:55 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) "," (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r3_euclidlp :::"are_lindependent2"::: ) ) ")" ))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); let "L" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Const "n"))); func :::"dist_v"::: "(" "x" "," "L" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: EUCLIDLP:def 5 "{" (Set ($#k12_euclid :::"|."::: ) (Set "(" "x" ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) ) where x0 "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") : (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) "L") "}" ; end; :: deftheorem defines :::"dist_v"::: EUCLIDLP:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k2_euclidlp :::"dist_v"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) ) where x0 "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) : (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" )))); definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); let "L" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Const "n"))); func :::"dist"::: "(" "x" "," "L" ")" -> ($#m1_subset_1 :::"Real":::) equals :: EUCLIDLP:def 6 (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k2_euclidlp :::"dist_v"::: ) "(" "x" "," "L" ")" ")" )); end; :: deftheorem defines :::"dist"::: EUCLIDLP:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k3_euclidlp :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k2_euclidlp :::"dist_v"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ")" )))))); theorem :: EUCLIDLP:56 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ))) "holds" (Bool "{" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) ) where x0 "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) : (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) "}" ($#r1_hidden :::"="::: ) (Set ($#k2_euclidlp :::"dist_v"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ))))) ; theorem :: EUCLIDLP:57 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "ex" (Set (Var "x0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_euclidlp :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" )) ")" ))))) ; theorem :: EUCLIDLP:58 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k3_euclidlp :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: EUCLIDLP:59 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "iff" (Bool (Set ($#k3_euclidlp :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "L1", "L2" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Const "n"))); pred "L1" :::"//"::: "L2" means :: EUCLIDLP:def 7 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "st" (Bool "(" (Bool "L1" ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool "L2" ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r2_euclidlp :::"//"::: ) (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")))) ")" )); symmetry (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Const "n"))) "st" (Bool (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "L2")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r2_euclidlp :::"//"::: ) (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")))) ")" ))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))) "st" (Bool "(" (Bool (Set (Var "L2")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "L1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r2_euclidlp :::"//"::: ) (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")))) ")" ))) ; end; :: deftheorem defines :::"//"::: EUCLIDLP:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2"))) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "L2")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r2_euclidlp :::"//"::: ) (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")))) ")" )) ")" ))); theorem :: EUCLIDLP:60 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L0")) "," (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L0")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L1"))) & (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L0")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2"))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "L1", "L2" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Const "n"))); pred "L1" :::"_|_"::: "L2" means :: EUCLIDLP:def 8 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "st" (Bool "(" (Bool "L1" ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool "L2" ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r4_euclidlp :::"_|_"::: ) (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")))) ")" )); symmetry (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Const "n"))) "st" (Bool (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "L2")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r4_euclidlp :::"_|_"::: ) (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")))) ")" ))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))) "st" (Bool "(" (Bool (Set (Var "L2")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "L1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r4_euclidlp :::"_|_"::: ) (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")))) ")" ))) ; end; :: deftheorem defines :::"_|_"::: EUCLIDLP:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2"))) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "L2")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r4_euclidlp :::"_|_"::: ) (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1")))) ")" )) ")" ))); theorem :: EUCLIDLP:61 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L0")) "," (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L0")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L1"))) & (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L0")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2"))))) ; theorem :: EUCLIDLP:62 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "L0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L0"))) & (Bool (Set (Var "L0")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L"))) & (Bool (Set (Var "L0")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "L"))) ")" ))))) ; theorem :: EUCLIDLP:63 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "L2")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L2")))) ")" )))) ; theorem :: EUCLIDLP:64 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "(" (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "L"))) & (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) ")" )))) ; theorem :: EUCLIDLP:65 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L1")) ($#r1_hidden :::"="::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2"))))) ; theorem :: EUCLIDLP:66 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2")))) "holds" (Bool "(" (Bool (Set (Var "L1")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L2")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) ")" ))) ; theorem :: EUCLIDLP:67 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2")))) "holds" (Bool "(" (Bool (Set (Var "L1")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L2")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) ")" ))) ; theorem :: EUCLIDLP:68 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) "holds" (Bool (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Var "L"))))))) ; theorem :: EUCLIDLP:69 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) "holds" (Bool "ex" (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ))) ")" )))))) ; theorem :: EUCLIDLP:70 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ))))))) ; theorem :: EUCLIDLP:71 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L1")) ($#r1_hidden :::"<>"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "L2"))))) ; theorem :: EUCLIDLP:72 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "L0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L0"))) & (Bool (Set (Var "L0")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L"))) ")" ))))) ; theorem :: EUCLIDLP:73 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "L0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L0"))) & (Bool (Set (Var "L0")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L"))) & (Bool (Set (Var "L0")) ($#r1_hidden :::"<>"::: ) (Set (Var "L"))) ")" ))))) ; theorem :: EUCLIDLP:74 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1"))) & (Bool (Set (Var "y0")) ($#r2_hidden :::"in"::: ) (Set (Var "L2"))) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set (Var "L2"))) & (Bool (Set (Var "y0")) ($#r1_hidden :::"<>"::: ) (Set (Var "y1"))) & (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x0"))) ($#r4_euclidlp :::"_|_"::: ) (Set (Set (Var "y1")) ($#k8_euclid :::"-"::: ) (Set (Var "y0"))))))) ; theorem :: EUCLIDLP:75 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L1")) ($#r1_hidden :::"<>"::: ) (Set (Var "L2"))))) ; theorem :: EUCLIDLP:76 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))))) ; theorem :: EUCLIDLP:77 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "y0")) "," (Set (Var "y1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1"))) & (Bool (Set (Var "y0")) ($#r2_hidden :::"in"::: ) (Set (Var "L2"))) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set (Var "L2"))) & (Bool (Set (Var "y0")) ($#r1_hidden :::"<>"::: ) (Set (Var "y1"))) & (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x0"))) ($#r2_euclidlp :::"//"::: ) (Set (Set (Var "y1")) ($#k8_euclid :::"-"::: ) (Set (Var "y0"))))))) ; theorem :: EUCLIDLP:78 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "x3")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) "," (Set (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r3_euclidlp :::"are_lindependent2"::: ) ) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "y3")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x3")) ")" )) & (Bool (Set (Var "L1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set (Var "L2")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y2")) "," (Set (Var "y3")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ))) & (Bool (Set (Set (Var "y3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ))) ")" )) ")" )))) ; theorem :: EUCLIDLP:79 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L2")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L1")) ($#r1_hidden :::"<>"::: ) (Set (Var "L2")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L2")))) ")" )))) ; theorem :: EUCLIDLP:80 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2")))) "holds" (Bool "ex" (Set (Var "L0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L0"))) & (Bool (Set (Var "L0")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L0")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L1"))) ")" ))))) ; theorem :: EUCLIDLP:81 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2")))) "holds" (Bool "ex" (Set (Var "x0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "x0"))) & (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))) & (Bool (Bool "not" (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "L2")))) ")" ))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x1", "x2", "x3" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); func :::"plane"::: "(" "x1" "," "x2" "," "x3" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) equals :: EUCLIDLP:def 9 "{" (Set (Var "x")) where x "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") : (Bool "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "a1")) ($#k7_real_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "a3"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) "x1" ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) "x2" ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) "x3" ")" ))) ")" )) "}" ; end; :: deftheorem defines :::"plane"::: EUCLIDLP:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) : (Bool "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "a1")) ($#k7_real_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "a3"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ))) ")" )) "}" ))); registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x1", "x2", "x3" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); cluster (Set ($#k4_euclidlp :::"plane"::: ) "(" "x1" "," "x2" "," "x3" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); attr "A" is :::"being_plane"::: means :: EUCLIDLP:def 10 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "st" (Bool "(" (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) "," (Set (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r3_euclidlp :::"are_lindependent2"::: ) ) & (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) ")" )); end; :: deftheorem defines :::"being_plane"::: EUCLIDLP:def 10 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_euclidlp :::"being_plane"::: ) ) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) "," (Set (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r3_euclidlp :::"are_lindependent2"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) ")" )) ")" ))); theorem :: EUCLIDLP:82 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) ")" ))) ; theorem :: EUCLIDLP:83 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ")" )) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ")" )) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ")" ))) "holds" (Bool (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ")" )))) ; theorem :: EUCLIDLP:84 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool "ex" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "c1")) ($#k7_real_1 :::"+"::: ) (Set (Var "c2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "c3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "c1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "c3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ))) ")" ))) "holds" (Bool (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ))))) ; theorem :: EUCLIDLP:85 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ))) "holds" (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )))) ; theorem :: EUCLIDLP:86 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_euclidlp :::"being_plane"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))) "holds" (Bool (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; theorem :: EUCLIDLP:87 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "a1")) ($#k7_real_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "a3"))) ($#r1_hidden :::"="::: ) (Num 1)))) "holds" (Bool (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ))))) ; theorem :: EUCLIDLP:88 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) "iff" (Bool "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "a1")) ($#k7_real_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "a3"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ))) ")" )) ")" ))) ; theorem :: EUCLIDLP:89 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "x3")) "," (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) "," (Set (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r3_euclidlp :::"are_lindependent2"::: ) ) & (Bool (Set (Set "(" (Set (Var "a1")) ($#k7_real_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "a3"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" ))) & (Bool (Set (Set "(" (Set (Var "b1")) ($#k7_real_1 :::"+"::: ) (Set (Var "b2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b1")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b3")) ($#k9_euclid :::"*"::: ) (Set (Var "x3")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Var "b3"))) ")" )))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"plane_of_REAL"::: "n" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) equals :: EUCLIDLP:def 11 "{" (Set (Var "P")) where P "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) : (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "st" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ))) "}" ; end; :: deftheorem defines :::"plane_of_REAL"::: EUCLIDLP:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "P")) where P "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) : (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ))) "}" )); registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) "n") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: EUCLIDLP:90 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n")))))) ; theorem :: EUCLIDLP:91 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))))) ; theorem :: EUCLIDLP:92 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) "," (Set (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) ($#r3_euclidlp :::"are_lindependent2"::: ) )) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" ))))) ; theorem :: EUCLIDLP:93 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "P1")) "is" ($#v1_euclidlp :::"being_plane"::: ) ) & (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Var "P2"))))) ; theorem :: EUCLIDLP:94 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x2")) "," (Set (Var "x3")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x3")) "," (Set (Var "x1")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) ")" ))) ; theorem :: EUCLIDLP:95 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "L1", "L2" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Const "n"))); pred "L1" "," "L2" :::"are_coplane"::: means :: EUCLIDLP:def 12 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "st" (Bool "(" (Bool "L1" ($#r1_tarski :::"c="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool "L2" ($#r1_tarski :::"c="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) ")" )); end; :: deftheorem defines :::"are_coplane"::: EUCLIDLP:def 12 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r7_euclidlp :::"are_coplane"::: ) ) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclidlp :::"plane"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ")" )) ")" )) ")" ))); theorem :: EUCLIDLP:96 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r7_euclidlp :::"are_coplane"::: ) ) "iff" (Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) ")" )) ")" ))) ; theorem :: EUCLIDLP:97 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r7_euclidlp :::"are_coplane"::: ) ))) ; theorem :: EUCLIDLP:98 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L2")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r7_euclidlp :::"are_coplane"::: ) ) & (Bool (Set (Var "L1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "L2")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "P")) "is" ($#v1_euclidlp :::"being_plane"::: ) ) ")" )))) ; theorem :: EUCLIDLP:99 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "L")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) ")" ))))) ; theorem :: EUCLIDLP:100 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "L")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "P")) "is" ($#v1_euclidlp :::"being_plane"::: ) ) ")" ))))) ; theorem :: EUCLIDLP:101 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "L")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool (Set (Var "P")) "is" ($#v1_euclidlp :::"being_plane"::: ) ))))) ; theorem :: EUCLIDLP:102 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P0")) "," (Set (Var "P1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) & (Bool (Set (Var "L")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P0"))) & (Bool (Set (Var "L")) ($#r1_tarski :::"c="::: ) (Set (Var "P0"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P1"))) & (Bool (Set (Var "L")) ($#r1_tarski :::"c="::: ) (Set (Var "P1")))) "holds" (Bool (Set (Var "P0")) ($#r1_hidden :::"="::: ) (Set (Var "P1"))))))) ; theorem :: EUCLIDLP:103 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L2")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r7_euclidlp :::"are_coplane"::: ) ) & (Bool (Set (Var "L1")) ($#r1_hidden :::"<>"::: ) (Set (Var "L2")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "P")) "is" ($#v1_euclidlp :::"being_plane"::: ) ) ")" )))) ; theorem :: EUCLIDLP:104 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L2")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L1")) ($#r1_hidden :::"<>"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "L2")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "P")) "is" ($#v1_euclidlp :::"being_plane"::: ) ) ")" )))) ; theorem :: EUCLIDLP:105 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L2")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L1")) ($#r1_hidden :::"<>"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Var "P2")))))) ; theorem :: EUCLIDLP:106 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L1")) ($#r1_hidden :::"<>"::: ) (Set (Var "L2")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "P")) "is" ($#v1_euclidlp :::"being_plane"::: ) ) ")" )))) ; theorem :: EUCLIDLP:107 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "L2")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_euclidlp :::"being_plane"::: ) ) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) ")" )))) ; theorem :: EUCLIDLP:108 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L0")) "," (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L0")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L0"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L1"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L0")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L0")) ($#r1_hidden :::"="::: ) (Set (Var "L1"))))))) ; theorem :: EUCLIDLP:109 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r7_euclidlp :::"are_coplane"::: ) ) & (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "L2"))))) ; theorem :: EUCLIDLP:110 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L1")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "L0")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L0")))) "holds" (Bool "(" (Bool (Set (Var "L0")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L0")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L1"))) ")" ))))) ; theorem :: EUCLIDLP:111 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L")) "," (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L1"))) & (Bool (Set (Var "L")) ($#r6_euclidlp :::"_|_"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2")))))) ; theorem :: EUCLIDLP:112 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L0")) "," (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L0")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L2")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "L0")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L1"))) & (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2"))) & (Bool (Set (Var "L0")) ($#r1_hidden :::"<>"::: ) (Set (Var "L1"))) & (Bool (Set (Var "L")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "L0"))) & (Bool (Set (Var "L")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "L1")))) "holds" (Bool (Set (Var "L")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "L2")))))) ; theorem :: EUCLIDLP:113 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclidlp :::"line_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r7_euclidlp :::"are_coplane"::: ) ) & (Bool (Set (Var "L1")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L2")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "L1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "L2")))) "holds" (Bool (Set (Var "L1")) ($#r5_euclidlp :::"//"::: ) (Set (Var "L2"))))) ; theorem :: EUCLIDLP:114 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_euclidlp :::"plane_of_REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1"))) "," (Set (Set (Var "y2")) ($#k8_euclid :::"-"::: ) (Set (Var "y1"))) ($#r3_euclidlp :::"are_lindependent2"::: ) )) "holds" (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ))))) ;