:: QUATERN3 semantic presentation begin theorem :: QUATERN3:1 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z1")) ")" )))) ; theorem :: QUATERN3:2 (Bool "for" (Set (Var "z")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool (Set (Set (Var "z")) ($#k26_quaterni :::"+"::: ) (Set (Var "z3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k23_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z3")) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k4_quatern2 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z3")) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z3")) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))) ; theorem :: QUATERN3:3 (Bool "for" (Set (Var "z")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool (Set (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set (Var "z3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z3")) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z3")) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z3")) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:4 (Bool "for" (Set (Var "z")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool (Set (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z3")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z3")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z3")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:5 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool (Set (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set ($#k4_quatern2 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:6 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool (Set (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:7 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool (Set (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:8 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set ($#k1_quatern2 :::"0q"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ; theorem :: QUATERN3:9 (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool (Set (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z"))))) ; theorem :: QUATERN3:10 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z"))))) ; theorem :: QUATERN3:11 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: QUATERN3:12 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" ) ($#k3_quatern2 :::".|"::: ) ))) ; theorem :: QUATERN3:13 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )))) ; theorem :: QUATERN3:14 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z")) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )))) ; theorem :: QUATERN3:15 (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z1")) ")" ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z1")) ($#k31_quaterni :::"*'"::: ) ")" )))) ; theorem :: QUATERN3:16 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z2")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z1")) ($#k31_quaterni :::"*'"::: ) ")" )))) ; theorem :: QUATERN3:17 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: QUATERN3:18 (Bool "for" (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k4_quatern2 :::""::: ) ) ($#k27_quaterni :::"*"::: ) (Set (Var "z1")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set ($#k4_quatern2 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:19 (Bool "for" (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k4_quatern2 :::""::: ) ) ($#k27_quaterni :::"*"::: ) (Set (Var "z1")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set ($#k4_quatern2 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:20 (Bool "for" (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k11_quaterni :::""::: ) ) ($#k27_quaterni :::"*"::: ) (Set (Var "z1")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:21 (Bool "for" (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k11_quaterni :::""::: ) ) ($#k27_quaterni :::"*"::: ) (Set (Var "z1")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:22 (Bool "for" (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k12_quaterni :::""::: ) ) ($#k27_quaterni :::"*"::: ) (Set (Var "z1")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:23 (Bool "for" (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k12_quaterni :::""::: ) ) ($#k27_quaterni :::"*"::: ) (Set (Var "z1")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:24 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" )))) ; theorem :: QUATERN3:25 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: QUATERN3:26 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: QUATERN3:27 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: QUATERN3:28 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:29 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:30 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z3")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: QUATERN3:31 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set "(" (Set (Var "z3")) ($#k27_quaterni :::"*"::: ) (Set (Var "z1")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )))) ; theorem :: QUATERN3:32 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" ) ($#k3_quatern2 :::".|"::: ) ))) ; theorem :: QUATERN3:33 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ))) ; theorem :: QUATERN3:34 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z3")) ($#k3_quatern2 :::".|"::: ) )))) ; theorem :: QUATERN3:35 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z3")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z3")) ($#k3_quatern2 :::".|"::: ) )))) ; theorem :: QUATERN3:36 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z3")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z3")) ($#k3_quatern2 :::".|"::: ) )))) ; theorem :: QUATERN3:37 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z3")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z3")) ($#k3_quatern2 :::".|"::: ) )))) ; theorem :: QUATERN3:38 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: QUATERN3:39 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z2")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: QUATERN3:40 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z2")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k3_quatern2 :::".|"::: ) ))) ; theorem :: QUATERN3:41 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) )))) ; theorem :: QUATERN3:42 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k3_quatern2 :::".|"::: ) )))) ; theorem :: QUATERN3:43 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERN3:44 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z2")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: QUATERN3:45 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k3_quatern2 :::".|"::: ) ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: QUATERN3:46 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" ) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z2")) ($#k8_quatern2 :::"""::: ) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z1")) ($#k8_quatern2 :::"""::: ) ")" )))) ; theorem :: QUATERN3:47 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k8_quatern2 :::"""::: ) ")" ) ($#k31_quaterni :::"*'"::: ) ))) ; theorem :: QUATERN3:48 (Bool (Set (Set ($#k2_quatern2 :::"1q"::: ) ) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_quatern2 :::"1q"::: ) )) ; theorem :: QUATERN3:49 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) )) & (Bool (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z1")) ($#k3_quatern2 :::".|"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "z1")) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k8_quatern2 :::"""::: ) ))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2")))) ; theorem :: QUATERN3:50 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z3")) ($#k26_quaterni :::"+"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: QUATERN3:51 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z3")) ($#k26_quaterni :::"+"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: QUATERN3:52 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z2"))))) ; theorem :: QUATERN3:53 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z2"))))) ; theorem :: QUATERN3:54 (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z2"))))) ; theorem :: QUATERN3:55 (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z2"))))) ; theorem :: QUATERN3:56 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z3")) ($#k29_quaterni :::"-"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: QUATERN3:57 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z3")) ($#k29_quaterni :::"-"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: QUATERN3:58 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z3"))))) ; theorem :: QUATERN3:59 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z3"))))) ; theorem :: QUATERN3:60 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z3"))))) ; theorem :: QUATERN3:61 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z3"))))) ; theorem :: QUATERN3:62 (Bool "for" (Set (Var "z1")) "," (Set (Var "z")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k26_quaterni :::"+"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2")))) ; theorem :: QUATERN3:63 (Bool "for" (Set (Var "z1")) "," (Set (Var "z")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k29_quaterni :::"-"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2")))) ; theorem :: QUATERN3:64 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z3")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z3")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: QUATERN3:65 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z3")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z3")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: QUATERN3:66 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z3")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z3")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: QUATERN3:67 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z3")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z3")) ($#k27_quaterni :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: QUATERN3:68 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z2")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z3")) ")" )))) ; theorem :: QUATERN3:69 (Bool "for" (Set (Var "z3")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z3")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z3")) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z2")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" )))) ; theorem :: QUATERN3:70 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z3")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z4")) ($#k29_quaterni :::"-"::: ) (Set (Var "z3")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k26_quaterni :::"+"::: ) (Set (Var "z1"))))) ; theorem :: QUATERN3:71 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z3")) ($#k29_quaterni :::"-"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z2")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z4")) ($#k29_quaterni :::"-"::: ) (Set (Var "z3")) ")" )))) ; theorem :: QUATERN3:72 (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k29_quaterni :::"-"::: ) (Set (Var "z1"))))) ; theorem :: QUATERN3:73 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:74 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z1")) ($#k6_quatern2 :::"/"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k3_quatern2 :::"|."::: ) (Set (Var "z2")) ($#k3_quatern2 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:75 (Bool (Set (Set ($#k4_quatern2 :::""::: ) ) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set ($#k4_quatern2 :::""::: ) ))) ; theorem :: QUATERN3:76 (Bool (Set (Set ($#k11_quaterni :::""::: ) ) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set ($#k11_quaterni :::""::: ) ))) ; theorem :: QUATERN3:77 (Bool (Set (Set ($#k12_quaterni :::""::: ) ) ($#k8_quatern2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set ($#k12_quaterni :::""::: ) ))) ; definitionlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "z" :::"^2"::: -> ($#m1_hidden :::"set"::: ) equals :: QUATERN3:def 1 (Set "z" ($#k27_quaterni :::"*"::: ) "z"); end; :: deftheorem defines :::"^2"::: QUATERN3:def 1 : (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k1_quatern3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z"))))); registrationlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "z" ($#k1_quatern3 :::"^2"::: ) ) -> ($#v1_quaterni :::"quaternion"::: ) ; end; definitionlet "z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); :: original: :::"^2"::: redefine func "z" :::"^2"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERN3:78 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k1_quatern3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERN3:79 (Bool (Set (Set ($#k1_quatern2 :::"0q"::: ) ) ($#k2_quatern3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: QUATERN3:80 (Bool (Set (Set ($#k2_quatern2 :::"1q"::: ) ) ($#k2_quatern3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: QUATERN3:81 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k1_quatern3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z")) ")" ) ($#k2_quatern3 :::"^2"::: ) ))) ; definitionlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "z" :::"^3"::: -> ($#m1_hidden :::"set"::: ) equals :: QUATERN3:def 2 (Set (Set "(" "z" ($#k27_quaterni :::"*"::: ) "z" ")" ) ($#k27_quaterni :::"*"::: ) "z"); end; :: deftheorem defines :::"^3"::: QUATERN3:def 2 : (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k3_quatern3 :::"^3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z")) ")" ) ($#k27_quaterni :::"*"::: ) (Set (Var "z"))))); registrationlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "z" ($#k3_quatern3 :::"^3"::: ) ) -> ($#v1_quaterni :::"quaternion"::: ) ; end; definitionlet "z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); :: original: :::"^3"::: redefine func "z" :::"^3"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERN3:82 (Bool (Set (Set ($#k1_quatern2 :::"0q"::: ) ) ($#k4_quatern3 :::"^3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: QUATERN3:83 (Bool (Set (Set ($#k2_quatern2 :::"1q"::: ) ) ($#k4_quatern3 :::"^3"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: QUATERN3:84 (Bool (Set (Set ($#k4_quatern2 :::""::: ) ) ($#k4_quatern3 :::"^3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set ($#k4_quatern2 :::""::: ) ))) ; theorem :: QUATERN3:85 (Bool (Set (Set ($#k11_quaterni :::""::: ) ) ($#k4_quatern3 :::"^3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set ($#k11_quaterni :::""::: ) ))) ; theorem :: QUATERN3:86 (Bool (Set (Set ($#k12_quaterni :::""::: ) ) ($#k4_quatern3 :::"^3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set ($#k12_quaterni :::""::: ) ))) ; theorem :: QUATERN3:87 (Bool (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set ($#k2_quatern2 :::"1q"::: ) ) ")" ) ($#k2_quatern3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: QUATERN3:88 (Bool (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set ($#k2_quatern2 :::"1q"::: ) ) ")" ) ($#k4_quatern3 :::"^3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ; theorem :: QUATERN3:89 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k3_quatern3 :::"^3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z")) ")" ) ($#k4_quatern3 :::"^3"::: ) ")" )))) ;