:: EUCLID_8 semantic presentation begin definitionlet "x", "y", "z" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"<*"::: redefine func :::"|[":::"x" "," "y" "," "z":::"]|"::: -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)); end; theorem :: EUCLID_8:1 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:2 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Num 3))) "holds" (Bool (Set (Var "f")) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)))) ; definitionfunc :::""::: -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) equals :: EUCLID_8:def 1 (Set ($#k1_euclid_8 :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) ); func :::""::: -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) equals :: EUCLID_8:def 2 (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) ); func :::""::: -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) equals :: EUCLID_8:def 3 (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_euclid_8 :::"]|"::: ) ); end; :: deftheorem defines :::""::: EUCLID_8:def 1 : (Bool (Set ($#k2_euclid_8 :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) )); :: deftheorem defines :::""::: EUCLID_8:def 2 : (Bool (Set ($#k3_euclid_8 :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) )); :: deftheorem defines :::""::: EUCLID_8:def 3 : (Bool (Set ($#k4_euclid_8 :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_euclid_8 :::"]|"::: ) )); definitionlet "p1", "p2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)); func "p1" :::""::: "p2" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) equals :: EUCLID_8:def 4 (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" "p1" ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" "p2" ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" "p1" ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" "p2" ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" "p1" ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" "p2" ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" "p1" ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" "p2" ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" "p1" ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" "p2" ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" "p1" ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" "p2" ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ); end; :: deftheorem defines :::""::: EUCLID_8:def 4 : (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))); theorem :: EUCLID_8:3 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r3_euclidlp :::"are_ldependent2"::: ) )) "holds" (Bool (Set (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k16_euclid :::"0.REAL"::: ) (Num 3)))) ; begin theorem :: EUCLID_8:4 (Bool (Set ($#k12_euclid :::"|."::: ) (Set ($#k2_euclid_8 :::""::: ) ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: EUCLID_8:5 (Bool (Set ($#k12_euclid :::"|."::: ) (Set ($#k3_euclid_8 :::""::: ) ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: EUCLID_8:6 (Bool (Set ($#k12_euclid :::"|."::: ) (Set ($#k4_euclid_8 :::""::: ) ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: EUCLID_8:7 (Bool (Set ($#k2_euclid_8 :::""::: ) ) "," (Set ($#k3_euclid_8 :::""::: ) ) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ; theorem :: EUCLID_8:8 (Bool (Set ($#k2_euclid_8 :::""::: ) ) "," (Set ($#k4_euclid_8 :::""::: ) ) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ; theorem :: EUCLID_8:9 (Bool (Set ($#k3_euclid_8 :::""::: ) ) "," (Set ($#k4_euclid_8 :::""::: ) ) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ; theorem :: EUCLID_8:10 (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set ($#k2_euclid_8 :::""::: ) ) "," (Set ($#k2_euclid_8 :::""::: ) ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: EUCLID_8:11 (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set ($#k3_euclid_8 :::""::: ) ) "," (Set ($#k3_euclid_8 :::""::: ) ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: EUCLID_8:12 (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set ($#k4_euclid_8 :::""::: ) ) "," (Set ($#k4_euclid_8 :::""::: ) ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: EUCLID_8:13 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_8:14 canceled; theorem :: EUCLID_8:15 canceled; theorem :: EUCLID_8:16 (Bool (Set (Set ($#k2_euclid_8 :::""::: ) ) ($#k5_euclid_8 :::""::: ) (Set ($#k3_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_8 :::""::: ) )) ; theorem :: EUCLID_8:17 (Bool (Set (Set ($#k3_euclid_8 :::""::: ) ) ($#k5_euclid_8 :::""::: ) (Set ($#k4_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_8 :::""::: ) )) ; theorem :: EUCLID_8:18 (Bool (Set (Set ($#k4_euclid_8 :::""::: ) ) ($#k5_euclid_8 :::""::: ) (Set ($#k2_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_euclid_8 :::""::: ) )) ; theorem :: EUCLID_8:19 (Bool (Set (Set ($#k4_euclid_8 :::""::: ) ) ($#k5_euclid_8 :::""::: ) (Set ($#k3_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid :::"-"::: ) (Set ($#k2_euclid_8 :::""::: ) ))) ; theorem :: EUCLID_8:20 (Bool (Set (Set ($#k2_euclid_8 :::""::: ) ) ($#k5_euclid_8 :::""::: ) (Set ($#k4_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid :::"-"::: ) (Set ($#k3_euclid_8 :::""::: ) ))) ; theorem :: EUCLID_8:21 (Bool (Set (Set ($#k3_euclid_8 :::""::: ) ) ($#k5_euclid_8 :::""::: ) (Set ($#k2_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid :::"-"::: ) (Set ($#k4_euclid_8 :::""::: ) ))) ; theorem :: EUCLID_8:22 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "p")) ($#k5_euclid_8 :::""::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:23 canceled; theorem :: EUCLID_8:24 canceled; theorem :: EUCLID_8:25 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "r")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:26 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "r")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:27 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "r")) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:28 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Num 1) ($#k9_euclid :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))) ; theorem :: EUCLID_8:29 canceled; theorem :: EUCLID_8:30 canceled; theorem :: EUCLID_8:31 (Bool (Set ($#k6_euclid :::"-"::: ) (Set ($#k2_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) )) ; theorem :: EUCLID_8:32 (Bool (Set ($#k6_euclid :::"-"::: ) (Set ($#k3_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) )) ; theorem :: EUCLID_8:33 (Bool (Set ($#k6_euclid :::"-"::: ) (Set ($#k4_euclid_8 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k1_euclid_8 :::"]|"::: ) )) ; theorem :: EUCLID_8:34 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k9_euclid :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:35 canceled; theorem :: EUCLID_8:36 canceled; theorem :: EUCLID_8:37 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))) ; theorem :: EUCLID_8:38 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" ))))) ; theorem :: EUCLID_8:39 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_euclid_8 :::"]|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "y")) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "z")) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))) ; theorem :: EUCLID_8:40 (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_euclid_8 :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))) ; theorem :: EUCLID_8:41 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k6_euclid :::"-"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_euclid :::"-"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))) ; theorem :: EUCLID_8:42 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k6_euclid :::"-"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_euclid_8 :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_euclid :::"-"::: ) (Set "(" (Set (Var "x")) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "y")) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "z")) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))) ; theorem :: EUCLID_8:43 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "p1")) ($#k7_euclid :::"+"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))) ; theorem :: EUCLID_8:44 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "p1")) ($#k8_euclid :::"-"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))) ; theorem :: EUCLID_8:45 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_euclid_8 :::"]|"::: ) ) ($#k7_euclid :::"+"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k1_euclid_8 :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "y1")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "x2")) ($#k9_binop_2 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "x3")) ($#k9_binop_2 :::"+"::: ) (Set (Var "y3")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))) ; theorem :: EUCLID_8:46 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_euclid_8 :::"]|"::: ) ) ($#k8_euclid :::"-"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k1_euclid_8 :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k10_binop_2 :::"-"::: ) (Set (Var "y1")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "x2")) ($#k10_binop_2 :::"-"::: ) (Set (Var "y2")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "x3")) ($#k10_binop_2 :::"-"::: ) (Set (Var "y3")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))) ; theorem :: EUCLID_8:47 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "p3")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "p3")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "p3")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" ))) "iff" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "p3")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "p3")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "p3")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" ))) ")" )) ; definitionlet "f1", "f2", "f3" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"VFunc"::: "(" "f1" "," "f2" "," "f3" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) means :: EUCLID_8:def 5 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" "f1" ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) "," (Set "(" "f2" ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) "," (Set "(" "f3" ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))); end; :: deftheorem defines :::"VFunc"::: EUCLID_8:def 5 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid_8 :::"VFunc"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) "," (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) "," (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))) ")" ))); theorem :: EUCLID_8:48 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k6_euclid_8 :::"VFunc"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" ))))) ; theorem :: EUCLID_8:49 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_euclid_8 :::"VFunc"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))) "iff" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")))) ")" ) ")" )))) ; theorem :: EUCLID_8:50 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Num 3))) ")" )) ; theorem :: EUCLID_8:51 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k11_finseq_1 :::"*>"::: ) ))) ; theorem :: EUCLID_8:52 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) )))) ; theorem :: EUCLID_8:53 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k6_euclid :::"-"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) "," (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:54 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) ; theorem :: EUCLID_8:55 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "p")) ($#k7_euclid :::"+"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:56 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_euclid_8 :::"VFunc"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_euclid_8 :::"VFunc"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t2")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t2")))) & (Bool (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t2")))) & (Bool (Set (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t2")))) ")" )))) ; theorem :: EUCLID_8:57 (Bool "for" (Set (Var "f1")) "," (Set (Var "g1")) "," (Set (Var "f2")) "," (Set (Var "g2")) "," (Set (Var "f3")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t2")))) & (Bool (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t2")))) & (Bool (Set (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t2"))))) "holds" (Bool (Set (Set "(" ($#k6_euclid_8 :::"VFunc"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_euclid_8 :::"VFunc"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t2")))))) ; theorem :: EUCLID_8:58 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) )))) ; theorem :: EUCLID_8:59 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_euclid_8 :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ($#k1_euclid_8 :::"]|"::: ) )))) ; theorem :: EUCLID_8:60 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k6_euclid :::"-"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) "," (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:61 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_seq_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ))) & (Bool (Set (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_seq_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ))) ")" )) ; theorem :: EUCLID_8:62 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "p1")) ($#k8_euclid :::"-"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p1")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:63 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" )))) ; theorem :: EUCLID_8:64 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: EUCLID_8:65 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: EUCLID_8:66 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))))) ; theorem :: EUCLID_8:67 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set "(" (Set (Var "r1")) ($#k9_euclid :::"*"::: ) (Set (Var "p")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k9_euclid :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))))) ; theorem :: EUCLID_8:68 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "p1")) ")" ) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_8:69 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set "(" (Set (Var "r1")) ($#k9_euclid :::"*"::: ) (Set (Var "p")) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k9_euclid :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k10_binop_2 :::"-"::: ) (Set (Var "r2")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))))) ; theorem :: EUCLID_8:70 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "p")) ")" ) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ) ")" ))))) ; theorem :: EUCLID_8:71 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set "(" ($#k16_euclid :::"0.REAL"::: ) (Num 3) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_8:72 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "p1")) ")" ) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_8:73 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "p1")) ")" ) "," (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "p2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ))) ; theorem :: EUCLID_8:74 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k8_euclid :::"-"::: ) (Set (Var "p2")) ")" ) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_8:75 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k7_euclid :::"+"::: ) (Set (Var "p2")) ")" ) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_8:76 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set "(" (Set (Var "r1")) ($#k9_euclid :::"*"::: ) (Set (Var "p1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k9_euclid :::"*"::: ) (Set (Var "p2")) ")" ) ")" ) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ))))) ; theorem :: EUCLID_8:77 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k7_euclid :::"+"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q1")) ($#k7_euclid :::"+"::: ) (Set (Var "q2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_8:78 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k8_euclid :::"-"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q1")) ($#k8_euclid :::"-"::: ) (Set (Var "q2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_8:79 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k16_euclid :::"0.REAL"::: ) (Num 3))) ")" )) ; theorem :: EUCLID_8:80 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k16_euclid :::"0.REAL"::: ) (Num 3))) ")" )) ; theorem :: EUCLID_8:81 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p")) ($#k8_euclid :::"-"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "p")) ($#k8_euclid :::"-"::: ) (Set (Var "q")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_8:82 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p")) ($#k7_euclid :::"+"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "p")) ($#k7_euclid :::"+"::: ) (Set (Var "q")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_8:83 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k5_euclid_8 :::""::: ) (Set (Var "p1")) ")" )))) ; theorem :: EUCLID_8:84 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_euclid_8 :::"]|"::: ) ) ($#k5_euclid_8 :::""::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k1_euclid_8 :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "x2")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y3")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x3")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y2")) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "x3")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y1")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y3")) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "x1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y2")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x2")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y1")) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))) ; theorem :: EUCLID_8:85 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "p1")) ")" ) ($#k5_euclid_8 :::""::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "p2")) ")" ))) & (Bool (Set (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "p1")) ")" ) ($#k5_euclid_8 :::""::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "p2")) ")" ))) ")" ))) ; theorem :: EUCLID_8:86 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set "(" (Set (Var "p2")) ($#k7_euclid :::"+"::: ) (Set (Var "p3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "p2")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "p3")) ")" )))) ; theorem :: EUCLID_8:87 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set "(" (Set (Var "p1")) ($#k7_euclid :::"+"::: ) (Set (Var "p2")) ")" ) ($#k5_euclid_8 :::""::: ) (Set (Var "p3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "p3")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k5_euclid_8 :::""::: ) (Set (Var "p3")) ")" )))) ; theorem :: EUCLID_8:88 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set "(" (Set (Var "p1")) ($#k7_euclid :::"+"::: ) (Set (Var "p2")) ")" ) ($#k5_euclid_8 :::""::: ) (Set "(" (Set (Var "q1")) ($#k7_euclid :::"+"::: ) (Set (Var "q2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "q1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "q2")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k5_euclid_8 :::""::: ) (Set (Var "q1")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k5_euclid_8 :::""::: ) (Set (Var "q2")) ")" )))) ; theorem :: EUCLID_8:89 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set "(" (Set (Var "p2")) ($#k5_euclid_8 :::""::: ) (Set (Var "p3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_euclid :::"*"::: ) (Set (Var "p2")) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_euclid :::"*"::: ) (Set (Var "p3")) ")" )))) ; definitionlet "p1", "p2", "p3" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)); func :::"|{":::"p1" "," "p2" "," "p3":::"}|"::: -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: EUCLID_8:def 6 (Set ($#k23_rvsum_1 :::"|("::: ) "p1" "," (Set "(" "p2" ($#k5_euclid_8 :::""::: ) "p3" ")" ) ($#k23_rvsum_1 :::")|"::: ) ); end; :: deftheorem defines :::"|{"::: EUCLID_8:def 6 : (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k7_euclid_8 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k7_euclid_8 :::"}|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set "(" (Set (Var "p2")) ($#k5_euclid_8 :::""::: ) (Set (Var "p3")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ))); theorem :: EUCLID_8:90 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k7_euclid_8 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#k7_euclid_8 :::"}|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_8:91 (Bool "for" (Set (Var "p2")) "," (Set (Var "p1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k7_euclid_8 :::"|{"::: ) (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#k7_euclid_8 :::"}|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_8:92 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k7_euclid_8 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p2")) ($#k7_euclid_8 :::"}|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_8:93 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k7_euclid_8 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k7_euclid_8 :::"}|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_euclid_8 :::"|{"::: ) (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p1")) ($#k7_euclid_8 :::"}|"::: ) ))) ; theorem :: EUCLID_8:94 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k7_euclid_8 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k7_euclid_8 :::"}|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k5_euclid_8 :::""::: ) (Set (Var "p2")) ")" ) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ))) ; theorem :: EUCLID_8:95 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k7_euclid_8 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) ($#k7_euclid_8 :::"}|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "q")) ($#k5_euclid_8 :::""::: ) (Set (Var "p1")) ")" ) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ))) ; begin definitionlet "f1", "f2", "f3" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "t0" be ($#m1_subset_1 :::"Real":::); func :::"VFuncdiff"::: "(" "f1" "," "f2" "," "f3" "," "t0" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) equals :: EUCLID_8:def 7 (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" "f1" "," "t0" ")" ")" ) "," (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" "f2" "," "t0" ")" ")" ) "," (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" "f3" "," "t0" ")" ")" ) ($#k1_euclid_8 :::"]|"::: ) ); end; :: deftheorem defines :::"VFuncdiff"::: EUCLID_8:def 7 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) "," (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) "," (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k1_euclid_8 :::"]|"::: ) )))); theorem :: EUCLID_8:96 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" ))))) ; theorem :: EUCLID_8:97 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g1")) ")" ) "," (Set "(" (Set (Var "f2")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g2")) ")" ) "," (Set "(" (Set (Var "f3")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k7_euclid :::"+"::: ) (Set "(" ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ))))) ; theorem :: EUCLID_8:98 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g1")) ")" ) "," (Set "(" (Set (Var "f2")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g2")) ")" ) "," (Set "(" (Set (Var "f3")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k8_euclid :::"-"::: ) (Set "(" ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ))))) ; theorem :: EUCLID_8:99 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) "," (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) "," (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" )))))) ; theorem :: EUCLID_8:100 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) "," (Set "(" (Set (Var "f2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) "," (Set "(" (Set (Var "f3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ($#k7_euclid :::"+"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))))) ; theorem :: EUCLID_8:101 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "g1")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f1")) ")" ) "," (Set "(" (Set (Var "g2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f2")) ")" ) "," (Set "(" (Set (Var "g3")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) )))) ; theorem :: EUCLID_8:102 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "g1")) ")" ) "," (Set "(" (Set (Var "f2")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "g2")) ")" ) "," (Set "(" (Set (Var "f3")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "g3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) )))) ; theorem :: EUCLID_8:103 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k6_rfunct_1 :::"^"::: ) ")" ) "," (Set "(" (Set (Var "f2")) ($#k6_rfunct_1 :::"^"::: ) ")" ) "," (Set "(" (Set (Var "f3")) ($#k6_rfunct_1 :::"^"::: ) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid :::"-"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))))) ; theorem :: EUCLID_8:104 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) "," (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) "," (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )))))) ; theorem :: EUCLID_8:105 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g1")) ")" ) ")" ) "," (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f2")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g2")) ")" ) ")" ) "," (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f3")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g3")) ")" ) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" )))))) ; theorem :: EUCLID_8:106 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g1")) ")" ) ")" ) "," (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f2")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g2")) ")" ) ")" ) "," (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f3")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g3")) ")" ) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" )))))) ; theorem :: EUCLID_8:107 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) "," (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) "," (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f3")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ")" )))))) ; theorem :: EUCLID_8:108 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f1")) ")" ) "," (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f2")) ")" ) "," (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) )))))) ; theorem :: EUCLID_8:109 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "g1")) ")" ) "," (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "g2")) ")" ) "," (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f3")) ")" ) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "g3")) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) )))))) ; theorem :: EUCLID_8:110 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f3")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k12_binop_2 :::"/"::: ) (Set (Var "r")) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ")" )))))) ; theorem :: EUCLID_8:111 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set "(" (Set (Var "f2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "f3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ($#k7_euclid :::"+"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))))) ; theorem :: EUCLID_8:112 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "h1")) "," (Set (Var "h2")) "," (Set (Var "h3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "h1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "h2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "h3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set (Var "h1")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "h2")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "h3")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ")" ) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ($#k7_euclid :::"+"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))))) ; theorem :: EUCLID_8:113 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "h1")) "," (Set (Var "h2")) "," (Set (Var "h3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "h1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "h2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "h3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set "(" (Set "(" (Set (Var "h2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f3")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "h3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f3")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "h1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ($#k7_euclid :::"+"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))))) ; theorem :: EUCLID_8:114 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "h1")) "," (Set (Var "h2")) "," (Set (Var "h3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "f3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "g3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "h1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "h2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0"))) & (Bool (Set (Var "h3")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "t0")))) "holds" (Bool (Set ($#k8_euclid_8 :::"VFuncdiff"::: ) "(" (Set "(" (Set "(" (Set (Var "h2")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "h3")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "h3")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "h1")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "h1")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "h2")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g3")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f3")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g2")) ")" ) ")" ) ")" ) ")" ) "," (Set (Var "t0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g3")) "," (Set (Var "t0")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "t0")) ")" ")" ) ")" ) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ($#k7_euclid :::"+"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "h3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "h1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h3")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h1")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "h2")) "," (Set (Var "t0")) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f3")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "g2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t0")) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))))) ;