fof(t6_algstr_3,theorem,( 0 = k1_rlvect_1(k4_algstr_3) ), inference(mizar_proof,[status(thm)],[d2_rlvect_1]), [file(algstr_3,t6_algstr_3),interesting(1.00)]). fof(l19_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k4_algstr_3)) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_algstr_3)) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_algstr_3)) => ( k1_algstr_3(k4_algstr_3,A,B,C) = k1_algstr_3(k4_algstr_3,A,B,D) => C = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_algstr_3,t5_algstr_3,t2_xcmplx_1]), [file(algstr_3,l19_algstr_3),interesting(0.88)]). fof(l21_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k4_algstr_3)) => ( A != B => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_algstr_3)) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_algstr_3)) => ? [E] : ( m1_subset_1(E,u1_struct_0(k4_algstr_3)) & k1_algstr_3(k4_algstr_3,A,E,C) = k1_algstr_3(k4_algstr_3,B,E,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_algstr_3,t5_algstr_3]), [file(algstr_3,l21_algstr_3),interesting(0.81)]). fof(t3_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,k1_numbers) => ~ ( A != B & ! [E] : ( m1_subset_1(E,k1_numbers) => k3_real_1(k4_real_1(A,E),C) != k3_real_1(k4_real_1(B,E),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t88_xcmplx_1]), [file(algstr_3,t3_algstr_3),interesting(0.71)]). fof(l16_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k4_algstr_3)) => k1_algstr_3(k4_algstr_3,A,k1_rlvect_1(k4_algstr_3),B) = B ) ) ), inference(mizar_proof,[status(thm)],[t6_algstr_3,d4_algstr_3]), [file(algstr_3,l16_algstr_3),interesting(0.61)]). fof(l17_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k4_algstr_3)) => k1_algstr_3(k4_algstr_3,k1_rlvect_1(k4_algstr_3),A,B) = B ) ) ), inference(mizar_proof,[status(thm)],[t6_algstr_3,d4_algstr_3]), [file(algstr_3,l17_algstr_3),interesting(0.61)]). fof(l18_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k4_algstr_3)) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_algstr_3)) => ? [D] : ( m1_subset_1(D,u1_struct_0(k4_algstr_3)) & k1_algstr_3(k4_algstr_3,A,B,D) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_algstr_3]), [file(algstr_3,l18_algstr_3),interesting(0.49)]). fof(t11_algstr_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_algstr_3(A) & l1_algstr_3(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( B != k1_rlvect_1(A) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & k1_algstr_3(A,B,E,C) = D ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_algstr_3,d7_algstr_3]), [file(algstr_3,t11_algstr_3),interesting(0.45)]). fof(t13_algstr_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_algstr_3(A) & l1_algstr_3(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( B != k1_rlvect_1(A) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & k1_algstr_3(A,E,B,C) = D ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_algstr_3,d7_algstr_3]), [file(algstr_3,t13_algstr_3),interesting(0.45)]). fof(l14_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => k1_algstr_3(k4_algstr_3,A,k2_algstr_3(k4_algstr_3),k1_rlvect_1(k4_algstr_3)) = A ) ), inference(mizar_proof,[status(thm)],[t6_algstr_3,d4_algstr_3]), [file(algstr_3,l14_algstr_3),interesting(0.44)]). fof(l15_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => k1_algstr_3(k4_algstr_3,k2_algstr_3(k4_algstr_3),A,k1_rlvect_1(k4_algstr_3)) = A ) ), inference(mizar_proof,[status(thm)],[t6_algstr_3,d4_algstr_3]), [file(algstr_3,l15_algstr_3),interesting(0.44)]). fof(l22_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k4_algstr_3)) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_algstr_3)) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_algstr_3)) => ! [E] : ( m1_subset_1(E,u1_struct_0(k4_algstr_3)) => ! [F] : ( m1_subset_1(F,u1_struct_0(k4_algstr_3)) => ~ ( k1_algstr_3(k4_algstr_3,C,A,E) = k1_algstr_3(k4_algstr_3,D,A,F) & k1_algstr_3(k4_algstr_3,C,B,E) = k1_algstr_3(k4_algstr_3,D,B,F) & A != B & C != D ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_algstr_3,t29_xcmplx_1,t5_xcmplx_1]), [file(algstr_3,l22_algstr_3),interesting(0.43)]). fof(t12_algstr_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_algstr_3(A) & l1_algstr_3(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( k1_algstr_3(A,B,C,D) = k1_algstr_3(A,B,E,D) => ( B = k1_rlvect_1(A) | C = E ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_algstr_3,d7_algstr_3]), [file(algstr_3,t12_algstr_3),interesting(0.36)]). fof(t14_algstr_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_algstr_3(A) & l1_algstr_3(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( k1_algstr_3(A,C,B,D) = k1_algstr_3(A,E,B,D) => ( B = k1_rlvect_1(A) | C = E ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_algstr_3,d7_algstr_3]), [file(algstr_3,t14_algstr_3),interesting(0.36)]). fof(t8_algstr_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_algstr_3(A) & l1_algstr_3(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( ( k1_algstr_3(A,D,B,E) = k1_algstr_3(A,F,B,G) & k1_algstr_3(A,D,C,E) = k1_algstr_3(A,F,C,G) ) => ( B = C | ( D = F & E = G ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_algstr_3,d7_algstr_3]), [file(algstr_3,t8_algstr_3),interesting(0.31)]). fof(l20_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k4_algstr_3)) => ( A != B => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_algstr_3)) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_algstr_3)) => ? [E] : ( m1_subset_1(E,u1_struct_0(k4_algstr_3)) & ? [F] : ( m1_subset_1(F,u1_struct_0(k4_algstr_3)) & k1_algstr_3(k4_algstr_3,E,A,F) = C & k1_algstr_3(k4_algstr_3,E,B,F) = D ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_algstr_3,d4_algstr_3,t88_xcmplx_1]), [file(algstr_3,l20_algstr_3),interesting(0.29)]). fof(d2_rlvect_1,definition,( ! [A] : ( l2_struct_0(A) => k1_rlvect_1(A) = u2_struct_0(A) ) ), file(rlvect_1,d2_rlvect_1), [interesting(0.00)]). fof(d4_algstr_3,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k3_zfmisc_1(k1_numbers,k1_numbers,k1_numbers),k1_numbers) & m2_relset_1(A,k3_zfmisc_1(k1_numbers,k1_numbers,k1_numbers),k1_numbers) ) => ( A = k3_algstr_3 <=> ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,k1_numbers) => k2_multop_1(k1_numbers,k1_numbers,k1_numbers,k1_numbers,A,B,C,D) = k3_real_1(k4_real_1(B,C),D) ) ) ) ) ) ), file(algstr_3,d4_algstr_3), [interesting(0.00)]). fof(t5_algstr_3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k4_algstr_3)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k4_algstr_3)) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_algstr_3)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ( ( A = D & B = E & C = F ) => k1_algstr_3(k4_algstr_3,A,B,C) = k3_real_1(k4_real_1(D,E),F) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_algstr_3]), [file(algstr_3,t5_algstr_3),interesting(0.00)]). fof(t2_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ( k2_xcmplx_0(A,B) = k2_xcmplx_0(C,B) => A = C ) ) ) ) ), file(xcmplx_1,t2_xcmplx_1), [interesting(0.00)]). fof(t88_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ), file(xcmplx_1,t88_xcmplx_1), [interesting(0.00)]). fof(t29_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k6_xcmplx_0(k2_xcmplx_0(A,B),C) = k2_xcmplx_0(k6_xcmplx_0(A,C),B) ) ) ) ), file(xcmplx_1,t29_xcmplx_1), [interesting(0.00)]). fof(t5_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ( k3_xcmplx_0(B,A) = k3_xcmplx_0(C,A) => ( A = 0 | B = C ) ) ) ) ) ), file(xcmplx_1,t5_xcmplx_1), [interesting(0.00)]). fof(t10_algstr_3,theorem,( $true ), file(algstr_3,t10_algstr_3), [interesting(0.00)]). fof(d7_algstr_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_algstr_3(A) ) => ( v2_algstr_3(A) <=> ( k1_rlvect_1(A) != k2_algstr_3(A) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k1_algstr_3(A,B,k2_algstr_3(A),k1_rlvect_1(A)) = B ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k1_algstr_3(A,k2_algstr_3(A),B,k1_rlvect_1(A)) = B ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k1_algstr_3(A,B,k1_rlvect_1(A),C) = C ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k1_algstr_3(A,k1_rlvect_1(A),B,C) = C ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & k1_algstr_3(A,B,C,E) = D ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( k1_algstr_3(A,B,C,D) = k1_algstr_3(A,B,C,E) => D = E ) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( B != C => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & k1_algstr_3(A,F,B,G) = D & k1_algstr_3(A,F,C,G) = E ) ) ) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( B != C => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & k1_algstr_3(A,B,F,D) = k1_algstr_3(A,C,F,E) ) ) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( k1_algstr_3(A,D,B,F) = k1_algstr_3(A,E,B,G) & k1_algstr_3(A,D,C,F) = k1_algstr_3(A,E,C,G) & B != C & D != E ) ) ) ) ) ) ) ) ) ) ), file(algstr_3,d7_algstr_3), [interesting(0.00)]). fof(t1_algstr_3,theorem,( $true ), file(algstr_3,t1_algstr_3), [interesting(0.00)]). fof(t2_algstr_3,theorem,( $true ), file(algstr_3,t2_algstr_3), [interesting(0.00)]). fof(t4_algstr_3,theorem,( $true ), file(algstr_3,t4_algstr_3), [interesting(0.00)]). fof(t7_algstr_3,theorem,( 1 = k2_algstr_3(k4_algstr_3) ), file(algstr_3,t7_algstr_3), [interesting(0.00)]). fof(t9_algstr_3,theorem,( $true ), file(algstr_3,t9_algstr_3), [interesting(0.00)]).