:: EC_PF_2 semantic presentation begin theorem :: EC_PF_2:1 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a2"))))) "holds" (Bool (Set (Set (Var "a1")) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k2_binom :::"|^"::: ) (Num 2))))) ; theorem :: EC_PF_2:2 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K"))))) ; theorem :: EC_PF_2:3 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a2")) "," (Set (Var "a4")) "," (Set (Var "a1")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "a2")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "a4")) ($#k11_algstr_0 :::"""::: ) ")" )))) "holds" (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")))))) ; theorem :: EC_PF_2:4 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a2")) "," (Set (Var "a4")) "," (Set (Var "a1")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3"))))) "holds" (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "a2")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "a4")) ($#k11_algstr_0 :::"""::: ) ")" ))))) ; theorem :: EC_PF_2:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "a1")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))) ; theorem :: EC_PF_2:6 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a2"))))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))))) ; theorem :: EC_PF_2:7 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a4")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a1")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")))) ")" ))) ; theorem :: EC_PF_2:8 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a5"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a5")) ")" ))) ")" ))) ; theorem :: EC_PF_2:9 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "a6")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a5")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a6"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a5")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a6")) ")" ))))) ; theorem :: EC_PF_2:10 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a4")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a1")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")))) ")" ))) ; theorem :: EC_PF_2:11 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a5"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a5")) ")" ))) ")" ))) ; theorem :: EC_PF_2:12 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "a6")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a5")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a6"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a5")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a6")) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a5")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a6"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a5")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a6")))) ")" ))) ; theorem :: EC_PF_2:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "a2")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "a3")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" )))))) ; theorem :: EC_PF_2:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ))) & (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ))) & (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ))) & (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ))) & (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ))) & (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ))) & (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a2")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a3")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ))) & (Bool (Set (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a2")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a4")) ")" ))) ")" ))) ; theorem :: EC_PF_2:15 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ))))) ; theorem :: EC_PF_2:16 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ))))) ; theorem :: EC_PF_2:17 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ))))) ; definitionlet "n", "p" be ($#v7_ordinal1 :::"natural"::: ) ($#m1_hidden :::"number"::: ) ; attr "p" is "n" :::"_or_greater"::: means :: EC_PF_2:def 1 (Bool "n" ($#r1_xxreal_0 :::"<="::: ) "p"); end; :: deftheorem defines :::"_or_greater"::: EC_PF_2:def 1 : (Bool "for" (Set (Var "n")) "," (Set (Var "p")) "being" ($#v7_ordinal1 :::"natural"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "p")) "is" (Set (Var "n")) ($#v1_ec_pf_2 :::"_or_greater"::: ) ) "iff" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) ")" )); registration cluster ($#v1_ordinal1 :::"epsilon-transitive"::: ) ($#v2_ordinal1 :::"epsilon-connected"::: ) ($#v3_ordinal1 :::"ordinal"::: ) ($#v7_ordinal1 :::"natural"::: ) bbbadV1_XCMPLX_0() bbbadV1_XREAL_0() ($#v1_int_1 :::"integer"::: ) ($#v1_int_2 :::"prime"::: ) ($#v1_xxreal_0 :::"ext-real"::: ) (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: EC_PF_2:18 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "gi")) "," (Set (Var "gj")) "," (Set (Var "gij")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "gi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gj")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gij")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "gi")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "gj")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "gij")) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))))))) ; theorem :: EC_PF_2:19 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "gi")) "," (Set (Var "gj")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "gi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gj")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set (Var "gi")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "gj")) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))))))) ; theorem :: EC_PF_2:20 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "g2")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")))))) ; theorem :: EC_PF_2:21 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "gi")) "," (Set (Var "gj")) "," (Set (Var "gij")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "gi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gj")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gij")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "gi")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gj")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "gij")) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))))))) ; theorem :: EC_PF_2:22 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "gi")) "," (Set (Var "gj")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "gi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gj")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set (Var "gi")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gj")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ; theorem :: EC_PF_2:23 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "gi")) "," (Set (Var "gj")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "gi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gj")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set (Var "gi")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "gj")) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))))))) ; theorem :: EC_PF_2:24 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "g2")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: EC_PF_2:25 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "g2")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ))))) ; theorem :: EC_PF_2:26 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "g2")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ))))) ; theorem :: EC_PF_2:27 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "g2")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "c")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "d")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ))))) ; theorem :: EC_PF_2:28 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 2)) & (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Var "g2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "g2")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) ")" )))) ; theorem :: EC_PF_2:29 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "g2")) "," (Set (Var "g3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set (Var "g3")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Var "g3")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "g3")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) ")" )))) ; begin definitionlet "p" be (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::); func :::"EC_WParam"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: EC_PF_2:def 2 "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) where a, b "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) : (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," "p" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ))) "}" ; end; :: deftheorem defines :::"EC_WParam"::: EC_PF_2:def 2 : (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) "holds" (Bool (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) where a, b "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) : (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) "}" )); registrationlet "p" be (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::); cluster (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) "p") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "p" be (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::); let "z" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Const "p"))); :: original: :::"`1"::: redefine func "z" :::"`1"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ); :: original: :::"`2"::: redefine func "z" :::"`2"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ); end; theorem :: EC_PF_2:30 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) ")" ))) ; definitionlet "p" be ($#m1_hidden :::"Prime":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ); let "P" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Const "a")) "," (Set (Const "b")) "," (Set (Const "p")) ")" ); func "P" :::"`1_3"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) means :: EC_PF_2:def 3 (Bool "for" (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "P" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "px")))); func "P" :::"`2_3"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) means :: EC_PF_2:def 4 (Bool "for" (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "P" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "py")))); func "P" :::"`3_3"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) means :: EC_PF_2:def 5 (Bool "for" (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "P" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "pz")))); end; :: deftheorem defines :::"`1_3"::: EC_PF_2:def 3 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) )) "iff" (Bool "for" (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Var "px")))) ")" ))))); :: deftheorem defines :::"`2_3"::: EC_PF_2:def 4 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) )) "iff" (Bool "for" (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Var "py")))) ")" ))))); :: deftheorem defines :::"`3_3"::: EC_PF_2:def 5 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) )) "iff" (Bool "for" (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "px")) "," (Set (Var "py")) "," (Set (Var "pz")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Var "pz")))) ")" ))))); theorem :: EC_PF_2:31 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) "," (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) "," (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) ))))) ; theorem :: EC_PF_2:32 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) "iff" (Bool "(" (Bool (Set (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k1_mcart_1 :::"`1_3"::: ) )) & (Bool (Set (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k2_mcart_1 :::"`2_3"::: ) )) & (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k3_mcart_1 :::"`3_3"::: ) )) ")" ) ")" ))))) ; theorem :: EC_PF_2:33 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Px")) "," (Set (Var "Py")) "," (Set (Var "Pz")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "Px")) "," (Set (Var "Py")) "," (Set (Var "Pz")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Px"))) & (Bool (Set (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Py"))) & (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "Pz"))) ")" )))) ; definitionlet "p" be ($#m1_hidden :::"Prime":::); let "P" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" )); let "CEQ" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ); pred "P" :::"is_on_curve"::: "CEQ" means :: EC_PF_2:def 6 (Bool (Set "CEQ" ($#k3_funct_2 :::"."::: ) "P") ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ))); end; :: deftheorem defines :::"is_on_curve"::: EC_PF_2:def 6 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) (Bool "for" (Set (Var "CEQ")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_2 :::"is_on_curve"::: ) (Set (Var "CEQ"))) "iff" (Bool (Set (Set (Var "CEQ")) ($#k3_funct_2 :::"."::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) ")" )))); theorem :: EC_PF_2:34 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_2 :::"is_on_curve"::: ) (Set ($#k5_ec_pf_1 :::"EC_WEqProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) "iff" (Bool (Set (Var "P")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) ")" )))) ; theorem :: EC_PF_2:35 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))))) ; definitionlet "p" be ($#m1_hidden :::"Prime":::); let "P" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" )); func :::"rep_pt"::: "P" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) equals :: EC_PF_2:def 7 (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" "P" ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" "P" ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k11_algstr_0 :::"""::: ) ")" ) ")" ) "," (Set "(" (Set "(" "P" ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" "P" ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k11_algstr_0 :::"""::: ) ")" ) ")" ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) if (Bool (Set "P" ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) if (Bool (Set "P" ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; end; :: deftheorem defines :::"rep_pt"::: EC_PF_2:def 7 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k11_algstr_0 :::"""::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k11_algstr_0 :::"""::: ) ")" ) ")" ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) )) ")" ")" ))); theorem :: EC_PF_2:36 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P"))) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "P"))) & (Bool (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" )) ")" )))) ; theorem :: EC_PF_2:37 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "st" (Bool (Bool (Set (Set "(" ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: EC_PF_2:38 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "st" (Bool (Bool (Set (Set "(" ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k11_algstr_0 :::"""::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k11_algstr_0 :::"""::: ) ")" ) ")" ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: EC_PF_2:39 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) "iff" (Bool (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "Q")))) ")" )))) ; begin definitionlet "p" be (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::); let "z" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Const "p"))); func :::"compell_ProjCo"::: "(" "z" "," "p" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" "z" ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," "p" ")" ")" ) "," (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" "z" ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," "p" ")" ")" ) means :: EC_PF_2:def 8 (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" "z" ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," "p" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) ))); end; :: deftheorem defines :::"compell_ProjCo"::: EC_PF_2:def 8 : (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) ")" )))); definitionlet "p" be (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::); let "z" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Const "p"))); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Const "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Const "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Const "p")) ")" ")" ) "," (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Const "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Const "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Const "p")) ")" ")" ); let "P" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Const "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Const "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Const "p")) ")" ); :: original: :::"."::: redefine func "F" :::"."::: "P" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" "z" ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," "p" ")" ); end; theorem :: EC_PF_2:40 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "O")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "O"))) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))))) ; theorem :: EC_PF_2:41 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "holds" (Bool (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set "(" (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "P")))))) ; theorem :: EC_PF_2:42 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set "(" (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P")) ")" )))))) ; theorem :: EC_PF_2:43 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) "iff" (Bool (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "Q")))) ")" )))) ; theorem :: EC_PF_2:44 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "P")))) "iff" (Bool (Set (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: EC_PF_2:45 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) )) & (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) )) ")" ) "iff" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) "or" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "Q")))) ")" ) ")" )))) ; theorem :: EC_PF_2:46 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) "iff" (Bool (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "P"))) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "Q")))) ")" )))) ; theorem :: EC_PF_2:47 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "Q")))) "iff" (Bool (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "P"))) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) ")" )))) ; theorem :: EC_PF_2:48 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_ec_pf_2 :::"rep_pt"::: ) (Set (Var "Q")) ")" ))) "iff" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "Q")))) ")" )))) ; theorem :: EC_PF_2:49 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" )))))) ; theorem :: EC_PF_2:50 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) "or" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "Q")))) ")" ) "iff" (Bool (Set (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ))) ")" )))) ; theorem :: EC_PF_2:51 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "Q"))))) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" )))))) ; theorem :: EC_PF_2:52 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q")))) & (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Set "(" ($#k8_ec_pf_2 :::"compell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ($#k9_ec_pf_2 :::"."::: ) (Set (Var "Q"))))) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" )))))) ; theorem :: EC_PF_2:53 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "g3")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: EC_PF_2:54 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k2_mcart_1 :::"`2_3"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )))))))) ; theorem :: EC_PF_2:55 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: EC_PF_2:56 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" )))))))) ; theorem :: EC_PF_2:57 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf1")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ")" ) ")" )))))))) ; theorem :: EC_PF_2:58 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "R")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: EC_PF_2:59 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g8")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "," (Set (Var "gf4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g3")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g4")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g8")) ($#r1_hidden :::"="::: ) (Set (Num 8) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")))) & (Bool (Set (Var "gf4")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf4")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k2_mcart_1 :::"`2_3"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )))))))) ; theorem :: EC_PF_2:60 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g8")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "," (Set (Var "gf4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g3")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g4")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g8")) ($#r1_hidden :::"="::: ) (Set (Num 8) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")))) & (Bool (Set (Var "gf4")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf4")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ")" )))))))) ; theorem :: EC_PF_2:61 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g8")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "," (Set (Var "gf4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g3")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g4")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g8")) ($#r1_hidden :::"="::: ) (Set (Num 8) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")))) & (Bool (Set (Var "gf4")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf4")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" )))))))) ; theorem :: EC_PF_2:62 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g8")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "," (Set (Var "gf4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g3")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g4")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g8")) ($#r1_hidden :::"="::: ) (Set (Num 8) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")))) & (Bool (Set (Var "gf4")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf4")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ")" )))))))) ; theorem :: EC_PF_2:63 (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g8")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "," (Set (Var "gf4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g3")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g4")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g8")) ($#r1_hidden :::"="::: ) (Set (Num 8) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")))) & (Bool (Set (Var "gf4")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf4")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "R")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "R")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))))))) ; definitionlet "p" be (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::); let "z" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Const "p"))); func :::"addell_ProjCo"::: "(" "z" "," "p" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" "z" ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," "p" ")" ")" ) "," (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" "z" ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," "p" ")" ")" ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" "z" ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," "p" ")" ")" ) means :: EC_PF_2:def 9 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "O")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" "z" ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," "p" ")" ) "st" (Bool (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) "implies" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) ")" & "(" (Bool (Bool (Set (Var "Q")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O"))) & (Bool (Bool "not" (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O"))))) "implies" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "P"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) & (Bool (Bool "not" (Set (Var "Q")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) & (Bool (Bool "not" (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))))) "implies" (Bool "for" (Set (Var "g2")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) "p")) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" )))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) & (Bool (Bool "not" (Set (Var "Q")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) & (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q")))) "implies" (Bool "for" (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g8")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "," (Set (Var "gf4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) "p")) & (Bool (Set (Var "g3")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_int_1 :::"mod"::: ) "p")) & (Bool (Set (Var "g4")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k6_int_1 :::"mod"::: ) "p")) & (Bool (Set (Var "g8")) ($#r1_hidden :::"="::: ) (Set (Num 8) ($#k6_int_1 :::"mod"::: ) "p")) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")))) & (Bool (Set (Var "gf4")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" )))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf4")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) ")" ")" )); end; :: deftheorem defines :::"addell_ProjCo"::: EC_PF_2:def 9 : (Bool "for" (Set (Var "p")) "being" (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Var "p"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ")" ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_ec_pf_2 :::"addell_ProjCo"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "O")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) "implies" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) ")" & "(" (Bool (Bool (Set (Var "Q")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O"))) & (Bool (Bool "not" (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O"))))) "implies" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "P"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) & (Bool (Bool "not" (Set (Var "Q")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) & (Bool (Bool "not" (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))))) "implies" (Bool "for" (Set (Var "g2")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" )))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "gf2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf3")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) & (Bool (Bool "not" (Set (Var "Q")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "O")))) & (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q")))) "implies" (Bool "for" (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g8")) "," (Set (Var "gf1")) "," (Set (Var "gf2")) "," (Set (Var "gf3")) "," (Set (Var "gf4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g3")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g4")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g8")) ($#r1_hidden :::"="::: ) (Set (Num 8) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "gf1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "gf2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k6_ec_pf_2 :::"`3_3"::: ) ")" ))) & (Bool (Set (Var "gf3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_ec_pf_2 :::"`1_3"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")))) & (Bool (Set (Var "gf4")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "gf1")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" )))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "g2")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf4")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "gf2")) ")" ) "," (Set "(" (Set "(" (Set (Var "gf1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set (Var "gf3")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "gf4")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k5_ec_pf_2 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "g8")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "gf2")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) ")" ")" )) ")" )))); definitionlet "p" be (Num 5) ($#v1_ec_pf_2 :::"_or_greater"::: ) ($#m1_hidden :::"Prime":::); let "z" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_ec_pf_2 :::"EC_WParam"::: ) (Set (Const "p"))); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Const "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Const "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Const "p")) ")" ")" ) "," (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Const "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Const "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Const "p")) ")" ")" ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Const "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Const "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Const "p")) ")" ")" ); let "Q", "R" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" (Set (Const "z")) ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" (Set (Const "z")) ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," (Set (Const "p")) ")" ); :: original: :::"."::: redefine func "F" :::"."::: "(" "Q" "," "R" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set "(" "z" ($#k2_ec_pf_2 :::"`1"::: ) ")" ) "," (Set "(" "z" ($#k3_ec_pf_2 :::"`2"::: ) ")" ) "," "p" ")" ); end;