:: QUATERN2 semantic presentation begin definition:: original: :::"0q"::: redefine func :::"0q"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; definition:: original: :::"1q"::: redefine func :::"1q"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERN2:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) ($#k6_quaterni :::"*]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k23_quaterni :::"+"::: ) (Set "(" (Set (Var "y")) ($#k25_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z")) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "w")) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))) ; theorem :: QUATERN2:2 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set (Var "c2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "c3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k26_quaterni :::"+"::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:3 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k26_quaterni :::"+"::: ) (Set ($#k1_quatern2 :::"0q"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ; theorem :: QUATERN2:4 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x3")) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x4")) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN2:5 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) ) ($#k29_quaterni :::"-"::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k9_real_1 :::"-"::: ) (Set (Var "y2")) ")" ) "," (Set "(" (Set (Var "x3")) ($#k9_real_1 :::"-"::: ) (Set (Var "y3")) ")" ) "," (Set "(" (Set (Var "x4")) ($#k9_real_1 :::"-"::: ) (Set (Var "y4")) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN2:6 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k29_quaterni :::"-"::: ) (Set (Var "c2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "c3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set (Var "c3")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "c2"))))) ; theorem :: QUATERN2:7 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set (Var "c2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "c2"))))) ; theorem :: QUATERN2:8 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k29_quaterni :::"-"::: ) (Set (Var "c2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "c2"))))) ; theorem :: QUATERN2:9 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ($#k25_quaterni :::"*"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set (Var "x1")) ($#k25_quaterni :::"*"::: ) (Set (Var "c")) ")" ))))) ; definitionlet "q" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"|."::: redefine func :::"|.":::"q":::".|"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; definition:: original: :::""::: redefine func :::""::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERN2:10 (Bool "for" (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERN2:11 (Bool (Set ($#k1_quatern2 :::"0q"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) )) ; theorem :: QUATERN2:12 (Bool "for" (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_quatern2 :::"0q"::: ) ) ($#k27_quaterni :::"*"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERN2:13 (Bool "for" (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k27_quaterni :::"*"::: ) (Set ($#k1_quatern2 :::"0q"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERN2:14 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k27_quaterni :::"*"::: ) (Set ($#k2_quatern2 :::"1q"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ; theorem :: QUATERN2:15 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_quatern2 :::"1q"::: ) ) ($#k27_quaterni :::"*"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ; theorem :: QUATERN2:16 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "c3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "c2")) ($#k27_quaterni :::"*"::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:17 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "c2")) ($#k26_quaterni :::"+"::: ) (Set (Var "c3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:18 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set (Var "c2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "c3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c3")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k27_quaterni :::"*"::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:19 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set ($#k2_quatern2 :::"1q"::: ) ) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "c"))))) ; theorem :: QUATERN2:20 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "c1")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c2")) ")" )))) ; theorem :: QUATERN2:21 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c2")) ")" )))) ; theorem :: QUATERN2:22 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "c1")) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c2"))))) ; theorem :: QUATERN2:23 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k29_quaterni :::"-"::: ) (Set (Var "c2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "c3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c3")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "c2")) ($#k27_quaterni :::"*"::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:24 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "c2")) ($#k29_quaterni :::"-"::: ) (Set (Var "c3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:25 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x3")) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x4")) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN2:26 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ; definitionlet "q", "r" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "q" :::"/"::: "r" -> ($#m1_hidden :::"set"::: ) means :: QUATERN2:def 1 (Bool "ex" (Set (Var "q0")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r0")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "q" ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "q0")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) ($#k6_quaterni :::"*]"::: ) )) & (Bool "r" ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "r0")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#k6_quaterni :::"*]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "r0")) ($#k8_real_1 :::"*"::: ) (Set (Var "q0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "q1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set (Var "q2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r3")) ($#k8_real_1 :::"*"::: ) (Set (Var "q3")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) "r" ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "r0")) ($#k8_real_1 :::"*"::: ) (Set (Var "q1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "q0")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set (Var "q3")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r3")) ($#k8_real_1 :::"*"::: ) (Set (Var "q2")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) "r" ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "r0")) ($#k8_real_1 :::"*"::: ) (Set (Var "q2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "q3")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set (Var "q0")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r3")) ($#k8_real_1 :::"*"::: ) (Set (Var "q1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) "r" ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "r0")) ($#k8_real_1 :::"*"::: ) (Set (Var "q3")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "q2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set (Var "q1")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r3")) ($#k8_real_1 :::"*"::: ) (Set (Var "q0")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) "r" ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" )); end; :: deftheorem defines :::"/"::: QUATERN2:def 1 : (Bool "for" (Set (Var "q")) "," (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k5_quatern2 :::"/"::: ) (Set (Var "r")))) "iff" (Bool "ex" (Set (Var "q0")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r0")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "q0")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "r0")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "r0")) ($#k8_real_1 :::"*"::: ) (Set (Var "q0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "q1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set (Var "q2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r3")) ($#k8_real_1 :::"*"::: ) (Set (Var "q3")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "r0")) ($#k8_real_1 :::"*"::: ) (Set (Var "q1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "q0")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set (Var "q3")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r3")) ($#k8_real_1 :::"*"::: ) (Set (Var "q2")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "r0")) ($#k8_real_1 :::"*"::: ) (Set (Var "q2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "q3")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set (Var "q0")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r3")) ($#k8_real_1 :::"*"::: ) (Set (Var "q1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "r0")) ($#k8_real_1 :::"*"::: ) (Set (Var "q3")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "q2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set (Var "q1")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r3")) ($#k8_real_1 :::"*"::: ) (Set (Var "q0")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" )) ")" ))); registrationlet "q", "r" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "q" ($#k5_quatern2 :::"/"::: ) "r") -> ($#v1_quaterni :::"quaternion"::: ) ; end; definitionlet "q", "r" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"/"::: redefine func "q" :::"/"::: "r" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERN2:27 (Bool "for" (Set (Var "q")) "," (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "q")) ($#k6_quatern2 :::"/"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "q")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "q")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k23_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "q")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k4_quatern2 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "q")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "q")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))) ; definitionlet "c" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "c" :::"""::: -> ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) equals :: QUATERN2:def 2 (Set (Set ($#k2_quatern2 :::"1q"::: ) ) ($#k6_quatern2 :::"/"::: ) "c"); end; :: deftheorem defines :::"""::: QUATERN2:def 2 : (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k7_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_quatern2 :::"1q"::: ) ) ($#k6_quatern2 :::"/"::: ) (Set (Var "c"))))); definitionlet "r" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"""::: redefine func "r" :::"""::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERN2:28 (Bool "for" (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k24_quaterni :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k4_quatern2 :::""::: ) ) ")" ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))) ; theorem :: QUATERN2:29 (Bool "for" (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "r")) ($#k8_quatern2 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "r")) ($#k8_quatern2 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "r")) ($#k8_quatern2 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "r")) ($#k8_quatern2 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" )) ; theorem :: QUATERN2:30 (Bool "for" (Set (Var "q")) "," (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "q")) ($#k6_quatern2 :::"/"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "q")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "q")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "q")) ($#k6_quatern2 :::"/"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "q")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "q")) ($#k6_quatern2 :::"/"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "q")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "q")) ($#k6_quatern2 :::"/"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "q")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "r")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" )) ; theorem :: QUATERN2:31 (Bool "for" (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "r")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "r")) ($#k8_quatern2 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: QUATERN2:32 (Bool "for" (Set (Var "r")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k8_quatern2 :::"""::: ) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: QUATERN2:33 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_quatern2 :::"0q"::: ) ))) "holds" (Bool (Set (Set (Var "c")) ($#k6_quatern2 :::"/"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k2_quatern2 :::"1q"::: ) ))) ; theorem :: QUATERN2:34 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "c")) ")" ) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set (Var "c")) ($#k8_quatern2 :::"""::: ) ")" )))) ; definitionfunc :::"compquaternion"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) means :: QUATERN2:def 3 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set (Var "c"))))); func :::"addquaternion"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) means :: QUATERN2:def 4 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set (Var "c2"))))); func :::"diffquaternion"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) means :: QUATERN2:def 5 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k29_quaterni :::"-"::: ) (Set (Var "c2"))))); func :::"multquaternion"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) means :: QUATERN2:def 6 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c2"))))); func :::"divquaternion"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) means :: QUATERN2:def 7 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k6_quatern2 :::"/"::: ) (Set (Var "c2"))))); func :::"invquaternion"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) means :: QUATERN2:def 8 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k8_quatern2 :::"""::: ) ))); end; :: deftheorem defines :::"compquaternion"::: QUATERN2:def 3 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k9_quatern2 :::"compquaternion"::: ) )) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set (Var "c"))))) ")" )); :: deftheorem defines :::"addquaternion"::: QUATERN2:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k10_quatern2 :::"addquaternion"::: ) )) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set (Var "c2"))))) ")" )); :: deftheorem defines :::"diffquaternion"::: QUATERN2:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k11_quatern2 :::"diffquaternion"::: ) )) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k29_quaterni :::"-"::: ) (Set (Var "c2"))))) ")" )); :: deftheorem defines :::"multquaternion"::: QUATERN2:def 6 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k12_quatern2 :::"multquaternion"::: ) )) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k27_quaterni :::"*"::: ) (Set (Var "c2"))))) ")" )); :: deftheorem defines :::"divquaternion"::: QUATERN2:def 7 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k13_quatern2 :::"divquaternion"::: ) )) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k6_quatern2 :::"/"::: ) (Set (Var "c2"))))) ")" )); :: deftheorem defines :::"invquaternion"::: QUATERN2:def 8 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k14_quatern2 :::"invquaternion"::: ) )) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k8_quatern2 :::"""::: ) ))) ")" )); definitionfunc :::"G_Quaternion"::: -> ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) means :: QUATERN2:def 9 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_quaterni :::"QUATERNION"::: ) )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k10_quatern2 :::"addquaternion"::: ) )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_quatern2 :::"0q"::: ) )) ")" ); end; :: deftheorem defines :::"G_Quaternion"::: QUATERN2:def 9 : (Bool "for" (Set (Var "b1")) "being" ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k15_quatern2 :::"G_Quaternion"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_quaterni :::"QUATERNION"::: ) )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_quatern2 :::"addquaternion"::: ) )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_quatern2 :::"0q"::: ) )) ")" ) ")" )); registration cluster (Set ($#k15_quatern2 :::"G_Quaternion"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ; end; registration cluster -> ($#v1_quaterni :::"quaternion"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k15_quatern2 :::"G_Quaternion"::: ) )); end; registrationlet "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k15_quatern2 :::"G_Quaternion"::: ) ); let "a", "b" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; theorem :: QUATERN2:35 (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k15_quatern2 :::"G_Quaternion"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_quatern2 :::"0q"::: ) )) ; registration cluster (Set ($#k15_quatern2 :::"G_Quaternion"::: ) ) -> ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; registrationlet "x" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k15_quatern2 :::"G_Quaternion"::: ) ); let "a" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; registrationlet "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k15_quatern2 :::"G_Quaternion"::: ) ); let "a", "b" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; theorem :: QUATERN2:36 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k15_quatern2 :::"G_Quaternion"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k15_quatern2 :::"G_Quaternion"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ; definitionfunc :::"R_Quaternion"::: -> ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) means :: QUATERN2:def 10 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_quaterni :::"QUATERNION"::: ) )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k10_quatern2 :::"addquaternion"::: ) )) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k12_quatern2 :::"multquaternion"::: ) )) & (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_quatern2 :::"1q"::: ) )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_quatern2 :::"0q"::: ) )) ")" ); end; :: deftheorem defines :::"R_Quaternion"::: QUATERN2:def 10 : (Bool "for" (Set (Var "b1")) "being" ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_quaterni :::"QUATERNION"::: ) )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_quatern2 :::"addquaternion"::: ) )) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k12_quatern2 :::"multquaternion"::: ) )) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_quatern2 :::"1q"::: ) )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_quatern2 :::"0q"::: ) )) ")" ) ")" )); registration cluster (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; registration cluster -> ($#v1_quaterni :::"quaternion"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k16_quatern2 :::"R_Quaternion"::: ) )); end; registrationlet "a", "b" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ); identify ; identify ; end; registration cluster (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) -> ($#v36_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ; end; theorem :: QUATERN2:37 (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_quatern2 :::"1q"::: ) )) ; theorem :: QUATERN2:38 (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_quatern2 :::"1q"::: ) )) ; theorem :: QUATERN2:39 (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_quatern2 :::"0q"::: ) )) ; registration cluster (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) -> ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v34_algstr_0 :::"almost_right_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ; end; registrationlet "x" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ); let "a" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; registrationlet "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ); let "a", "b" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; identify ; end; definitionlet "z" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ); :: original: :::"*'"::: redefine func "z" :::"*'"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ); end; theorem :: QUATERN2:40 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))))) ; theorem :: QUATERN2:41 (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) ")" ) ($#k17_quatern2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ))) ; theorem :: QUATERN2:42 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k17_quatern2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) )))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) )))) ; theorem :: QUATERN2:43 (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) ")" ) ($#k17_quatern2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ))) ; theorem :: QUATERN2:44 (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: QUATERN2:45 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) "st" (Bool (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) )))) ; theorem :: QUATERN2:46 (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: QUATERN2:47 (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ) ")" ) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k16_quatern2 :::"R_Quaternion"::: ) ))) ; definitionlet "x", "y" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "x" :::".|."::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) equals :: QUATERN2:def 11 (Set "x" ($#k27_quaterni :::"*"::: ) (Set "(" "y" ($#k31_quaterni :::"*'"::: ) ")" )); end; :: deftheorem defines :::".|."::: QUATERN2:def 11 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k18_quatern2 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "y")) ($#k31_quaterni :::"*'"::: ) ")" )))); theorem :: QUATERN2:48 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "c2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "c2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "c1")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "c2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "c1")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "c2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "c1")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "c1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "c2")) ")" ) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN2:49 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "c")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ))) ; theorem :: QUATERN2:50 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "c")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "c")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "c")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "c")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "c")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: QUATERN2:51 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "c1")) ($#k3_quatern2 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "c2")) ($#k3_quatern2 :::".|"::: ) )))) ; theorem :: QUATERN2:52 (Bool "for" (Set (Var "c")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "c")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERN2:53 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set (Var "c2")) ")" ) ($#k18_quatern2 :::".|."::: ) (Set (Var "c3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c3")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:54 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set "(" (Set (Var "c2")) ($#k26_quaterni :::"+"::: ) (Set (Var "c3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:55 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "c1")) ")" ) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2")) ")" )))) ; theorem :: QUATERN2:56 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "c2")) ")" )))) ; theorem :: QUATERN2:57 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "c1")) ")" ) ($#k18_quatern2 :::".|."::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2"))))) ; theorem :: QUATERN2:58 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k29_quaterni :::"-"::: ) (Set (Var "c2")) ")" ) ($#k18_quatern2 :::".|."::: ) (Set (Var "c3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c3")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "c2")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:59 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set "(" (Set (Var "c2")) ($#k29_quaterni :::"-"::: ) (Set (Var "c3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c3")) ")" )))) ; theorem :: QUATERN2:60 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set (Var "c2")) ")" ) ($#k18_quatern2 :::".|."::: ) (Set "(" (Set (Var "c1")) ($#k26_quaterni :::"+"::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c1")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2")) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c1")) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2")) ")" )))) ; theorem :: QUATERN2:61 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k29_quaterni :::"-"::: ) (Set (Var "c2")) ")" ) ($#k18_quatern2 :::".|."::: ) (Set "(" (Set (Var "c1")) ($#k29_quaterni :::"-"::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c1")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2")) ")" ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "c2")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c1")) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k18_quatern2 :::".|."::: ) (Set (Var "c2")) ")" )))) ;